{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T04:00:34Z","timestamp":1770436834263,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540278825","type":"print"},{"value":"9783540317142","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_18","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"253-268","source":"Crossref","is-referenced-by-count":25,"title":["Control Law Diagrams in Circus"],"prefix":"10.1007","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phil","family":"Clayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"O\u2019Halloran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"The MathWorks. Simulink, \n                    \n                      http:\/\/www.mathworks.com\/products\/simulink"},{"key":"18_CR2","first-page":"169","volume-title":"ICFEM 2000","author":"R. Arthan","year":"2000","unstructured":"Arthan, R., Caseley, P., O\u2019Halloran, C., Smith, A.: ClawZ: Control laws in Z. In: ICFEM 2000, pp. 169\u2013176. IEEE Press, Los Alamitos (2000)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-45648-1_21","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J. Blow","year":"2002","unstructured":"Blow, J., Galloway, A.: Generalised Substitution Language and Differentials. In: Bert, D., et al. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 396\u2013415. Springer, Heidelberg (2002)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-36580-X_11","volume-title":"Hybrid Systems: Computation and Control","author":"R.J. Boulton","year":"2003","unstructured":"Boulton, R.J., Hardy, R., Martin, U.: A Hoare-Logic for Single-Input Single-Output Continuous-Time Control Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 113\u2013125. Springer, Heidelberg (2003)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-45212-6_7","volume-title":"Embedded Software","author":"P. Caspi","year":"2003","unstructured":"Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating Discrete-Time Simulink to Lustre. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol.\u00a02855, pp. 84\u201399. Springer, Heidelberg (2003)"},{"issue":"2 - 3","key":"18_CR6","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A.L.C. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing\u00a015(2 - 3), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"issue":"3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650050016","volume":"10","author":"A.L.C. Cavalcanti","year":"1999","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC\u2014A Refinement Calculus for Z. Formal Aspects of Computing\u00a010(3), 267\u2013289 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"ZUM \u201998: The Z Formal Specification Notation","author":"C. Fischer","year":"1998","unstructured":"Fischer, C.: How to Combine Z with a Process Algebra. In: P. Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol.\u00a01493, pp. 5\u201325. Springer, Heidelberg (1998)"},{"key":"18_CR9","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"18_CR10","unstructured":"Jersak, M., Ziegenbein, D., Wolf, F., Richter, K., Ernst, R.: Embedded System Design using the SPI Workbench. In: 3rd International Forum on Design Languages (2000)"},{"key":"18_CR11","unstructured":"King, D.J., Arthan, R.D., Winnersh, I.C.L.: Development of Practical Verification Tools. ICL Systems Journal\u00a011(1) (1996)"},{"key":"18_CR12","unstructured":"Mahony, B.: Workshop on Formalising Continuous Mathematics. The DOVE Approach to the Design of Complex Dynamic Processes, 167\u2013187 (2002)"},{"key":"18_CR13","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"18_CR14","first-page":"127","volume-title":"ASE 1999","author":"C. O\u2019Halloran","year":"1999","unstructured":"O\u2019Halloran, C., Smith, A.: Verification of Picture Generated Code. In: ASE 1999, pp. 127\u2013136. IEEE Press, Los Alamitos (1999)"},{"key":"18_CR15","first-page":"281","volume-title":"CPA 2004","author":"M.V.M. Oliveira","year":"2004","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Refining Industrial Scale Systems in Circus. In: CPA 2004, September 2004, pp. 281\u2013309. IOS Press, Amsterdam (2004)"},{"key":"18_CR16","series-title":"Prentice-Hall Series in Computer Science","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"18_CR17","unstructured":"Spencer, C.: Model Checking for Stateflow Diagram with Floating Point Variables and Complex Expressions. Master\u2019s thesis, Carnegie Mellon University (2002)"},{"key":"18_CR18","unstructured":"Tiwari, A.: Formal Semantics and Analysis Methods for Simulink Stateflow Models. Technical report, SRI International (2002), \n                    \n                      http:\/\/www.csl.sri.com\/~tiwari\/stateflow.html"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.C.P. Woodcock","year":"2002","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of Circus. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 184\u2013203. Springer, Heidelberg (2002)"},{"key":"18_CR20","volume-title":"Using Z\u2014Specification, Refinement, and Proof","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z\u2014Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:47:52Z","timestamp":1619506072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11526841_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}