{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T21:42:27Z","timestamp":1757540547516},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752905"},{"type":"electronic","value":"9783540752929"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75292-9_6","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T06:43:07Z","timestamp":1189492987000},"page":"79-93","source":"Crossref","is-referenced-by-count":6,"title":["Stepwise Development of Simulink Models Using the Refinement Calculus Framework"],"prefix":"10.1007","author":[{"given":"Pontus","family":"Bostr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lionel","family":"Morel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marina","family":"Wald\u00e9n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems\u00a017(3), 507\u2013534 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0027228","volume-title":"Formal Methods for Industrial Applications","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R., B\u00f6rger, E., Langmaack, H.: The steam boiler case study: Competition of formal program specification and development methods. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Formal Methods for Industrial Applications. LNCS, vol.\u00a01165, pp. 1\u201312. Springer, Heidelberg (1996)"},{"key":"6_CR3","first-page":"169","volume-title":"Proceedings of ICFEM 2000","author":"R. Arthan","year":"2000","unstructured":"Arthan, R., Caseley, P., O\u2019Halloran, C., Smith, A.: ClawZ: Control laws in Z. In: Proceedings of ICFEM 2000, pp. 169\u2013176. IEEE Press, Los Alamitos (2000)"},{"key":"6_CR4","first-page":"131","volume-title":"Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium of Principles of Distributed Computing","author":"R.-J.R. Back","year":"1983","unstructured":"Back, R.-J.R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium of Principles of Distributed Computing, pp. 131\u2013142. ACM Press, New York (1983)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/BFb0015020","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R.-J.R. Back","year":"1994","unstructured":"Back, R.-J.R., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 367\u2013384. Springer, Heidelberg (1994)"},{"key":"6_CR6","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J.R. Back","year":"1998","unstructured":"Back, R.-J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s00165-003-0005-6","volume":"15","author":"R.-J.R. Back","year":"2003","unstructured":"Back, R.-J.R., von Wright, J.: Compositional action system refinement. Formal Aspects of Computing\u00a015, 103\u2013117 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR8","unstructured":"Bostr\u00f6m, P., Linjama, M., Morel, L., Siivonen, L., Wald\u00e9n, M.: Design and validation of digital controllers for hydraulics systems. In: The 10th Scandinavian International Conference on Fluid Power, Tampere, Finland (2007)"},{"key":"6_CR9","unstructured":"Bostr\u00f6m, P., Morel, L., Wald\u00e9n, M.: Stepwise development of Simulink models using the refinement calculus framework. Technical Report 821, TUCS (2007)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/11526841_18","volume-title":"FM 2005: Formal Methods","author":"A. Cavalanti","year":"2005","unstructured":"Cavalanti, A., Clayton, P., O\u2019Halloran, C.: Control law diagrams in Circus. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 253\u2013268. Springer, Heidelberg (2005)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/11901433_5","volume-title":"Formal Methods and Software Engineering","author":"C. Chen","year":"2006","unstructured":"Chen, C., Dong, J.S.: Applying timed interval calculus to Simulink diagrams. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 74\u201393. Springer, Heidelberg (2006)"},{"key":"6_CR12","unstructured":"Esterel Technologies. SCADE (2006), \n                  \n                     http:\/\/www.esterel-technologies.com\/"},{"issue":"9","key":"6_CR13","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"6_CR14","unstructured":"Mahony, B.: The DOVE approach to design of complex dynamic processes. In: Theorem Proving in Higher Order Logic, NASA conf. publ., CP-2002-211736 (2002)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Maraninchi, F., Morel, L.: Logical-time contracts for reactive embedded components. In: ECBSE 2004. 30th EUROMICRO Conference on Component-Based Software Engineering Track, Rennes, France (2004)","DOI":"10.1109\/EURMIC.2004.1333355"},{"key":"6_CR16","unstructured":"Mathworks Inc., Simulink\/Stateflow (2006), \n                  \n                    http:\/\/www.mathworks.com"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/11783596_19","volume-title":"Mathematics of Program Construction","author":"L. Meinicke","year":"2006","unstructured":"Meinicke, L., Hayes, I.: Continuous action system refinement. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 316\u2013337. Springer, Heidelberg (2006)"},{"key":"6_CR18","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"6_CR19","series-title":"ENTCS","volume-title":"SLAP 2005","author":"J. Mik\u00e1\u010d","year":"2005","unstructured":"Mik\u00e1\u010d, J., Caspi, P.: Temporal refinement for Lustre. In: SLAP 2005. Proceedings of Synchronous Languages, Applications and Programming, Edinburgh, Scotland. ENTCS, Elsevier, Amsterdam (2005)"},{"key":"6_CR20","unstructured":"Scilab Consortium. Scilab\/Scicos (2006), \n                  \n                    http:\/\/www.scilab.org"},{"issue":"1","key":"6_CR21","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/JPROC.2002.805818","volume":"91","author":"A. Tiwari","year":"2003","unstructured":"Tiwari, A., Shankar, N., Rushby, J.: Invisible formal methods for embedded control systems. Proceedings of the IEEE\u00a091(1), 29\u201339 (2003)","journal-title":"Proceedings of the IEEE"},{"issue":"4","key":"6_CR22","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1145\/1113830.1113834","volume":"4","author":"S. Tripakis","year":"2005","unstructured":"Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. on Embedded Computing Systems\u00a04(4), 779\u2013818 (2005)","journal-title":"ACM Trans. on Embedded Computing Systems"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:59:02Z","timestamp":1619506742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752905","9783540752929"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}