{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,24]],"date-time":"2024-06-24T15:52:02Z","timestamp":1719244322414},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,3,1]],"date-time":"2014-03-01T00:00:00Z","timestamp":1393632000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Simulink\u2019s Stateflow is a graphical notation widely adopted in industry. Since it is frequently used to model safety-critical systems, correctness of implementations of Stateflow charts is a major concern. In previous work, we have shown how we can generate formal models for refinement of Stateflow charts automatically. Here, we define a refinement strategy that supports the automated verification of implementations with respect to these models. We consider the verification of implementations that follow architectural patterns used in the Stateflow code generator. We present a detailed procedure for application of refinement laws. If the implementation is correct, the procedure succeeds. If a law application fails, the implementation is either incorrect or does not use the expected architectural pattern. The very low proof burden associated with the refinement verification makes a high level of automation possible.<\/jats:p>","DOI":"10.1007\/s00165-013-0291-6","type":"journal-article","created":{"date-parts":[[2013,12,14]],"date-time":"2013-12-14T13:54:12Z","timestamp":1387029252000},"page":"367-405","source":"Crossref","is-referenced-by-count":3,"title":["Refinement-based verification of implementations of Stateflow charts"],"prefix":"10.1145","volume":"26","author":[{"given":"Alvaro","family":"Miyazawa","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of York, Deramore Lane, Heslington, YO10 5GH, York, UK"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, Deramore Lane, Heslington, YO10 5GH, York, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Adams MM Clayton PB (2005) Cost-effective formal verification for control systems. In Lau K Banach R (eds) ICFEM 2005: formal methods and software engineering volume 3785 of Lecture Notes in Computer Science. Springer Berlin pp 465\u2013479","DOI":"10.1007\/11576280_32"},{"key":"e_1_2_1_2_3_2","volume-title":"High integrity software: the SPARK approach to safety and security","author":"Barnes J","year":"2003"},{"key":"e_1_2_1_2_4_2","unstructured":"Banphawatthanarak C Krogh BH (2000) Verification of stateflow diagrams using smv: sf2smv 2.0. Technical Report CMU-ECE-2000-020. Carnegie Mellon University"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti ALC Clayton P (2006) Verification of control systems using Circus . In: 11th IEEE international conference on engineering of complex computer systems. IEEE Computer Society New York pp 269\u2013278","DOI":"10.1109\/ICECCS.2006.1690376"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Caspi P Curic A Maignan A Sofronis C Tripakis S (2003) Translating discrete-time Simulink to Lustre. In: Alur R Lee I (eds) EMSOFT 2003 volume 2855 of Lecture Notes in Computer Science. Springer Berlin pp 84\u201399","DOI":"10.1007\/978-3-540-45212-6_7"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti ALC Clayton P O\u2019Halloran C (2005) Control law diagrams in Circus . In: Fitzgerald J Hayes IJ Tarlecki A (eds) FM 2005: formal methods volume 3582 of Lecture Notes in Computer Science. Springer Berlin pp 253\u2013268","DOI":"10.1007\/11526841_18"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0170-3"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0235-0"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0006-5"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050016"},{"key":"e_1_2_1_2_12_2","unstructured":"Ferrari A Fantechi A Bacherini S Zingoni N (2009) Modeling guidelines for code generation in the railway signaling context. In: NASA formal methods pp 166\u2013170"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_2_14_2","volume-title":"Unifying theories of programming","author":"Hoare CAR","year":"1998"},{"key":"e_1_2_1_2_15_2","unstructured":"Harel D Pnueli A Schmidt JP Sherman R (1987) On the formal semantics of statecharts. In: 2nd IEEE symposium on logic in computer science. IEEE Press New York pp 54\u201364"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Latella D Majzik I Massink M (1999) Towards a formal operational semantics of UML statechart diagrams. In: Ciancarini P Gorrieri R (eds) IFIP TC6\/WG6.1 third international conference on formal methods for open object-based distributed systems. Kluwer Dordrecht pp 331\u2013347","DOI":"10.1007\/978-0-387-35562-7_25"},{"key":"e_1_2_1_2_17_2","unstructured":"Lilius J Paltor IP (1999) The semantics Of UML state machines. Technical Report 273 Turku Centre and Computer Science"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Lublinerman R Szegedy C Tripakis S (2009) Modular code generation from synchronous block diagrams modularity versus code size. In: 36th symposium on principles of programming languages","DOI":"10.1145\/1480881.1480893"},{"key":"e_1_2_1_2_19_2","unstructured":"Mathworks Automotive Advisory Board. MAAB Control Algorithm Modeling. http:\/\/www.mathworks.co.uk\/help\/simulink\/maab-control-algorithm-modeling.html"},{"key":"e_1_2_1_2_20_2","unstructured":"The MathWorks Inc. Real-Time Workshop. www.mathworks.com\/products\/rtwt"},{"key":"e_1_2_1_2_21_2","unstructured":"The MathWorks Inc. Simulink. www.mathworks.com\/products\/simulink"},{"key":"e_1_2_1_2_22_2","unstructured":"The MathWorks Inc. Stateflow and Stateflow coder 7 user\u2019s guide. www.mathworks.com\/products"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Miyazawa A Cavalcanti ALC (2011) Refinement-based verification of sequential implementations of Stateflow charts. In: Derrick J Boiten E Reeves S (eds) Refinement workshop. Electronic Notes in Theoretical Computer Science. Elsevier. doi:10.4204\/EPTCS.55","DOI":"10.4204\/EPTCS.55.5"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.007"},{"key":"e_1_2_1_2_25_2","unstructured":"Miyazawa A (2012) Formal verification of implementations of Stateflow charts. PhD thesis University of York"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Mikk E Lakhnech Y Petersohn C Siegel M (1997) On formal semantics of Statecharts as supported by statemate. In: BCS-FACS northern formal methods workshop. Springer Berlin","DOI":"10.14236\/ewic\/FA1997.12"},{"key":"e_1_2_1_2_27_2","volume-title":"Programming from specifications","author":"Morgan CC","year":"1994","edition":"2"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"e_1_2_1_2_29_2","unstructured":"Ng MY Butler M (2003) Towards formalizing UML state diagrams in CSP. In: International conference on software engineering and formal methods. IEEE Computer Society Silver Spring pp 138\u2013148"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Oliveira MVM Cavalcanti ALC (2008) ArcAngelC: a refinement tactic language for Circus . Electron Notes Theor Comput Sci 214C:203\u2013229","DOI":"10.1016\/j.entcs.2008.06.010"},{"key":"e_1_2_1_2_31_2","unstructured":"Oliveira MVM (2006) Formal derivation of state-rich reactive programs using Circus . PhD thesis University of York"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.11.012"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Shalev M (1991) What is in a step: on the semantics of statecharts. In: Ito T Meyer AR (eds) Theoretical aspects of computer software volume 526 of Lecture Notes in Computer Science. Springer Berlin pp 244\u2013264","DOI":"10.1007\/3-540-54415-1_49"},{"key":"e_1_2_1_2_34_2","volume-title":"Understanding concurrent systems","author":"Roscoe AW","year":"2011"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Ramos R Sampaio ACA Mota AC (2005) A semantics for UML-RT active classes via mapping into Circus . In: Formal methods for open object-based distributed systems volume 3535 of Lecture Notes in Computer Science pp 99\u2013114","DOI":"10.1007\/11494881_7"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Snook C Savicks V Butler M (2011) Verification of UML models by translation to UML-B. In: 9th international conference on formal methods for components and objects volume 6957 of Lecture Notes in Computer Science. Springer Berlin pp 251\u2013266","DOI":"10.1007\/978-3-642-25271-6_13"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Scaife N Sofronis C Caspi P Tripakis S Maraninchi F (2004) Defining and translating a \u201cSafe\u201d subset of Simulink\/Stafeflow into Lustre. In: International conference on embedded software. ACM Press New york pp 259\u2013268","DOI":"10.1145\/1017753.1017795"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Sekerinski E Zurob R (2002) Translating statecharts to B. In: Butler M Petre L Sere K (eds) Integrated formal methods volume 2335 of Lecture Notes in Computer Science. Springer Berlin pp 128\u2013144","DOI":"10.1007\/3-540-47884-1_8"},{"key":"e_1_2_1_2_39_2","unstructured":"TargetLink. http:\/\/www.dspace.com\/en\/inc\/home\/products\/sw\/pcgs\/targetli.cfm. Accessed: 05 May 2013"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Toyn I Galloway A (2005) Proving properties of stateflow models using ISO Standard Z and CADiZ. In: Henson MC Treharne H King S Schneider S (eds) ZB 2005: formal specification and development in Z and B volume 3455 of Lecture Notes in Computer Science. Springer Berlin pp 104\u2013123","DOI":"10.1007\/11415787_7"},{"key":"e_1_2_1_2_41_2","unstructured":"Tiwari A (2002) Formal semantics and analysis methods for Simulink Stateflow models. Technical report SRI International. www.csl.sri.com\/~tiwari\/stateflow.html"},{"key":"e_1_2_1_2_42_2","unstructured":"Toom A Naks T Pantel M Gandriau M Indrawati (2008) Gene-auto: an automatic code generator for a safe subset of Simulink\/Stateflow and Scicos. In: 4th European congress ERTS embedded real-time software"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/s10270-002-0012-8","article-title":"A structured operational semantics for UML-statecharts","volume":"1","author":"Beeck M","year":"2002","journal-title":"Softw Syst Model"},{"key":"e_1_2_1_2_44_2","unstructured":"Woodcock JCP Davies J (1996) Using Z\u2014specification refinement and proof. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Cavalcanti A (2010) Encoding Circus programs in ProofPower-Z. In: Butterfield A (ed) Unifying theories of programming volume 5713 of Lecture Notes in Computer Science. Springer Berlin pp 218\u2013237","DOI":"10.1007\/978-3-642-14521-6_13"},{"issue":"1","key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/s00165-011-0218-z","article-title":"Mechanised support for sound refinement tactics","volume":"24","author":"Zeyda F","year":"2012","journal-title":"Formal Aspect Comput"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0291-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0291-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0291-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:04:45Z","timestamp":1641485085000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0291-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["10.1007\/s00165-013-0291-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0291-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3]]}}}