{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,20]],"date-time":"2025-12-20T02:17:15Z","timestamp":1766197035981,"version":"3.38.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"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":[[2011,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Control engineers make extensive use of diagrammatic notations; control law diagrams are used in industry every day. Techniques and tools for analysis of these diagrams or their models are plentiful, but verification of their implementations is a challenge that has been taken up by few. We are aware only of approaches that rely on automatic code generation, which is not enough assurance for certification, and often not adequate when tailored hardware components are used. Our work is based on<jats:italic>Circus<\/jats:italic>, a notation that combines Z, CSP, and a refinement calculus, and on industrial tools that produce partial Z and CSP models of discrete-time Simulink diagrams. We present a strategy to translate Simulink diagrams to<jats:italic>Circus<\/jats:italic>, and a strategy to prove that a parallel Ada implementation refines the<jats:italic>Circus<\/jats:italic>specification; we rely on a<jats:italic>Circus<\/jats:italic>semantics for the program. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of a large set of diagrams, and support verification of a large number of implementations. We can handle, for instance, arbitrarily large data types and dynamic scheduling.<\/jats:p>","DOI":"10.1007\/s00165-010-0170-3","type":"journal-article","created":{"date-parts":[[2011,1,10]],"date-time":"2011-01-10T13:02:07Z","timestamp":1294664527000},"page":"465-512","source":"Crossref","is-referenced-by-count":24,"title":["From control law diagrams to Ada via<i>Circus<\/i>"],"prefix":"10.1145","volume":"23","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[{"name":"University of York, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phil","family":"Clayton","sequence":"additional","affiliation":[{"name":"Systems Assurance Group, QinetiQ, Malvern, UK"},{"name":"Veonix, Worcester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"O\u2019Halloran","sequence":"additional","affiliation":[{"name":"Systems Assurance Group, QinetiQ, Malvern, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_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. Lecture notes in computer science vol 3785. Springer Berlin pp 465\u2013479","DOI":"10.1007\/11576280_32"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Arthan R Caseley P O\u2019Halloran CM Smith A (2000) ClawZ: control laws in Z. In: 3rd international conference on formal engineering methods. IEEE Press pp 169\u2013176","DOI":"10.1109\/ICFEM.2000.873817"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aldrich B Fehnker A Feiler PH Han Z Krogh BH Lim K Sivashankar S (2004) Managing verification activities using SVM. In: Davies J Schultte W Barnett M (eds) 6th international conference on formal engineering methods. Lecture notes in computer science vol 3308. Springer Berlin pp 61\u201375","DOI":"10.1007\/978-3-540-30482-1_13"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"volume-title":"Programming in Ada 95","year":"2005","author":"Barnes J","key":"e_1_2_1_2_5_2"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Basir N Denney E Fischer B (2010) Deriving safety cases for hierarchical structure in model-based development. In: Computer safety reliability and security. Lecture Notes in Computer Science vol 6351. Springer Berlin pp 68\u201381","DOI":"10.1007\/978-3-642-15651-9_6"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Blow J Galloway A (2002) Generalised substitution language and differentials. In: Bert D Bowen JP Henson MC Robinson K (eds) ZB 2002: Formal Specification and Development in Z and B. of Lecture notes in computer science vol 2272. Springer Berlin pp 396\u2013415","DOI":"10.1007\/3-540-45648-1_21"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Boulton RJ Gottliebsen H Hardy R Kelsy T Martin U (2004) Design verification for control engineering. In: Boiten EA Derrick J Smith G (eds) IFM 2004: integrated formal methods. Lecture notes in computer science vol 2999. Springer Berlin pp 21\u201335 Invited paper","DOI":"10.1007\/978-3-540-24756-2_2"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Boulton RJ Hardy R Martin U (2003) A hoare-logic for single-input single-output continuous-time control systems. In: 6th international workshop on hybrid systems: computation and control. Lecture notes in computer science vol 2623. Springer Berlin pp 113\u2013125","DOI":"10.1007\/3-540-36580-X_11"},{"key":"e_1_2_1_2_10_2","unstructured":"Bostr\u00f6m P Morel L Wald\u00e9n M (2007) Stepwise development of Simulink models using the refinement calculus framework. In: Woodcock JCP Jones CB Liu Z (eds) International colloquium on theoretical aspects of computing. Lecture notes in computer science vol 4711. Springer Berlin"},{"key":"e_1_2_1_2_11_2","unstructured":"Cavalcanti ALC (2008) Stateflow diagrams in Circus. In: Machado P (eds) SBMF 2008: Brazilian symposium on formal methods. In: Electronic notes in theoretical computer science. Elsevier Amsterdam (invited paper)"},{"key":"e_1_2_1_2_12_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 pp 269\u2013278","DOI":"10.1109\/ICECCS.2006.1690376"},{"key":"e_1_2_1_2_13_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. Lecture Notes in Computer Science vol 2855. Springer Berlin pp 84\u201399","DOI":"10.1007\/978-3-540-45212-6_7"},{"key":"e_1_2_1_2_14_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. Lecture notes in computer science vol 3582. Springer Berlin pp 253\u2013268","DOI":"10.1007\/11526841_18"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Chen C Dong JS (2006) Applying timed interval calculus to Simulink diagrams. In: Liu Z Jifeng H (eds) International conference on formal engineering methods. Lecture notes in computer science. Springer Berlin pp 74\u201393","DOI":"10.1007\/11901433_5"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0108-9"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0006-5"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050016"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Dajani-Brown S Cofer D Hartmann G Pratt S (2003) Formal modeling and analysis of an avionics triplex sensor voter. In: Ball T Rajamani SK (eds) SPIN 2003. Lecture notes in computer science vol 2648. Springer Berlin pp 34\u201348","DOI":"10.1007\/3-540-44829-2_3"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Freitas AF Cavalcanti ALC (2006) Automatic translation from Circus to Java. In: Misra J Nipkow T Sekerinski E (eds) FM 2006: formal methods. Lecture notes in computer science vol 4085. Springer Berlin pp 115\u2013130","DOI":"10.1007\/11813040_9"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Freitas LJS Cavalcanti ALC Woodcock JCP (2006) Taking our own medicine: applying the refinement calculus to state-rich refinement model checking. In: Liu Z He J (eds) Formal methods and software engineering. 8th international conference on formal engineering methods ICFEM 2006. Lecture notes in computer science vol 4260. Springer Berlin pp 697\u2013716","DOI":"10.1007\/11901433_38"},{"volume-title":"ZUM\u201998: the Z formal specification notation","year":"1998","author":"Fischer C","key":"e_1_2_1_2_22_2"},{"key":"e_1_2_1_2_23_2","unstructured":"Fischer C (2000) Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis Fachbereich Informatik Universit\u00e4t Oldenburg"},{"key":"#cr-split#-e_1_2_1_2_24_2.1","doi-asserted-by":"crossref","unstructured":"Fehnker A Krogh BH (2004) Hybrid system verification is not a sinecure: electronic throttle control case study. In: Wang F","DOI":"10.1007\/978-3-540-30476-0_23"},{"key":"#cr-split#-e_1_2_1_2_24_2.2","unstructured":"(ed) ATVA 2004. Lecture notes in computer science vol 3299. Springer Berlin pp 263-277"},{"key":"e_1_2_1_2_25_2","unstructured":"Freitas LJS (2006) Model checking Circus. PhD thesis University of York Department of Computer Science"},{"key":"#cr-split#-e_1_2_1_2_26_2.1","doi-asserted-by":"crossref","unstructured":"Giese H Hirsch M (2006) Modular verification of safe online-reconfiguration for proactive components in mechatronic UML. In: Bruel J-M","DOI":"10.1007\/11663430_8"},{"key":"#cr-split#-e_1_2_1_2_26_2.2","unstructured":"(ed) Satellite events at the MoDELS 2005 conference. Lecture Notes in Computer Science vol 1618. Springer Berlin pp 67-78"},{"key":"#cr-split#-e_1_2_1_2_27_2.1","doi-asserted-by":"crossref","unstructured":"Graf S Haugen O Ober I Selic B (2006) Modelling and analysis of real-time and embedded systems. In: Bruel J-M","DOI":"10.1007\/11663430_7"},{"key":"#cr-split#-e_1_2_1_2_27_2.2","unstructured":"(ed) Satellite events at the MoDELS 2005 conference. Lecture notes in computer science vol 1618. Springer Berlin pp 58-66"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Gurr C Tourlas K (2000) Towards the principled design of software engineering diagrams. In: 22nd international conference on software engineering. ACM Press pp 509\u20135188","DOI":"10.1145\/337180.337371"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Hammond K Michaelson G (2003) Hume: a domain-specific language for real-time embedded systems. In: Generative programming and component engineering. Lecture notes in computer science vol 2830. Springer Berlin pp 37\u201356","DOI":"10.1007\/978-3-540-39815-8_3"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Hoenick J Olderog E-R (2002) Combining specification techniques for processes data and time. In: Butler MJ Petre L Sere K (eds) Integrated formal methods. Lecture notes in computer science vol 2335 pp 245\u2013266","DOI":"10.1007\/3-540-47884-1_14"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Joshi A Heimdahl MPE (2005) Model-Based Safety Analysis of Simulink Models using SCADE Design Verifier. In: Winther R Gran Ba Dahll G editors SAFECOMP 2005 volume 3688 of Lecture Notes in Computer Science pages 122\u2013135. Springer-Verlag","DOI":"10.1007\/11563228_10"},{"key":"e_1_2_1_2_33_2","unstructured":"Jersak M Ziegenbein D Wolf F Richter K Ernst R Cieslok F Teich J Strehl K Thiele L (2000) Embedded system design using the SPI workbench. In: 3rd international forum on design languages"},{"key":"e_1_2_1_2_34_2","unstructured":"King DJ Arthan RD Winnersh ICL (1996) Development of practical verification tools. ICL Syst J 11(1)"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Krogh BH (1999) Approximating Hybrid System Dynamics for Analysis and Control. In: Vaandrager FW van Schuppen JH (eds) Hybrid systems: computation and control: second international workshop. Lecture notes in computer science vol 1569. Springer Berlin","DOI":"10.1007\/3-540-48983-5_2"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Krogh BH (1999) Recent developments in modeling and analysis of hybrid dynamic systems. In: Donatelli S Kleijn J (eds) Applications and theory of petri nets 1999: 20th international conference. Lecture notes in computer science vol 1639. Springer Berlin","DOI":"10.1007\/3-540-48745-X_7"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Kirsch CM Sanvido MAA (2002) A Giotto-based helicopter control system. In: Sangiovanni-Vincentelli A Sifakis J (eds) EMSOFT 2002. Lecture notes in computer science vol 2491. Springer Berlin pp 46\u201360","DOI":"10.1007\/3-540-45828-X_5"},{"key":"e_1_2_1_2_38_2","unstructured":"Mahony B (2002) 1st international workshop on formalising continuous mathematics. In: The DOVE approach to the design of complex dynamic processes pp 167\u2013187"},{"key":"e_1_2_1_2_39_2","unstructured":"The MathWorks Inc. Simulink. http:\/\/www.mathworks.com\/products\/simulink"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.841115"},{"key":"e_1_2_1_2_41_2","volume-title":"Programming from specifications","author":"Morgan CC","year":"1994","edition":"2"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0003-8"},{"issue":"2","key":"e_1_2_1_2_43_2","first-page":"126","article-title":"Formal development of industrial-scale systems","volume":"1","author":"Oliveira MVM","year":"2005","journal-title":"Innov Syst Softw Eng"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Oliveira MVM Cavalcanti ALC Woodcock JCP (2007) Unifying theories in ProofPowerZ. Formal Aspects Comput. doi:10.1007\/s00165-007-0044-5","DOI":"10.1007\/s00165-007-0044-5"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0052-5"},{"key":"e_1_2_1_2_46_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_47_2","unstructured":"Ranville S Black PE (2001) Automated testing requirements\u2014automotive perspective. In: 2nd international workshop on automated program analysis testing and verification"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0119-6"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Sherif A (2006) A Framework for Specification and Validation of Real-time Systems using Circus actions. PhD thesis Centro de Inform\u00e1tica\/UFPE Brazil","DOI":"10.1007\/978-3-540-31862-0_34"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Sherif A He Jifeng Cavalcanti ALC Sampaio ACA (2005) A framework for specification and validation of real-time systems using circus actions. In: Liu Z Araki K (eds) International colloquium on theoretical aspects of computing. Lecture notes in computer science vol 3407. Springer Berlin pp 478\u2013493","DOI":"10.1007\/978-3-540-31862-0_34"},{"key":"e_1_2_1_2_51_2","unstructured":"Spencer C (2002) Model checking for stateflow diagram with floating point variables and complex expressions. Master\u2019s thesis Department of Electrical and Computer Engineering Carnegie Mellon University"},{"key":"e_1_2_1_2_52_2","unstructured":"Tiwari A (2002) Formal semantics and analysis methods for Simulink stateflow models. Technical report SRI International. http:\/\/www.csl.sri.com\/~tiwari\/stateflow.html"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Tiwari A Khanna G (2002) Series of abstractions for hybrid automata. In: Vaandrager FW van Schuppen JH (eds) Hybrid systems: computation and control: second international workshop. Lecture notes in computer science vol 2289. Springer Berlin pp 465\u2013478","DOI":"10.1007\/3-540-45873-5_36"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Treharne H Schneider S (1999) Using a process algebra to control B operations. In: 1st international conference on integrated formal methods IFM\u201999. Springer Berlin pp 437\u2013457","DOI":"10.1007\/978-1-4471-0851-1_23"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805818"},{"volume-title":"Using Z\u2014specification, refinement, and proof","year":"1996","author":"Woodcock JCP","key":"e_1_2_1_2_56_2"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Cavalcanti ALC (2009) Mechanised translation of control law diagrams into Circus. In: Integrated formal methods. Lecture notes in computer science. Springer Berlin","DOI":"10.1007\/978-3-642-00255-7_11"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-010-0170-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-010-0170-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-010-0170-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T15:40:53Z","timestamp":1740843653000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-010-0170-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["10.1007\/s00165-010-0170-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-010-0170-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2011,7]]}}}