{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:28:57Z","timestamp":1791232137862,"version":"4.1.0"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2007,7,31]],"date-time":"2007-07-31T00:00:00Z","timestamp":1185840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transf"],"published-print":{"date-parts":[[2007,10,6]]},"DOI":"10.1007\/s10009-007-0049-7","type":"journal-article","created":{"date-parts":[[2007,7,30]],"date-time":"2007-07-30T06:34:03Z","timestamp":1185777243000},"page":"447-456","source":"Crossref","is-referenced-by-count":52,"title":["An operational semantics for Stateflow"],"prefix":"10.1007","volume":"9","author":[{"given":"Gr\u00e9goire","family":"Hamon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Rushby","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,7,31]]},"reference":[{"key":"49_CR1","unstructured":"Anton, J., da Costa, P., Errington, L.: Formal synthesis of generators for embedded systems. Technical report, Kestrel Technology (2005)"},{"key":"49_CR2","doi-asserted-by":"crossref","unstructured":"Banphawatthanarak, C., Krogh, B.H., Butts, K.: Symbolic verification of executable control specifications. In: Proceedings of the 10th IEEE International Symposium on Computer Aided Control System Design, pp. 581\u2013586. Kohala Coast\u2014Island of Hawai\u2019i, HI (1999)","DOI":"10.1109\/CACSD.1999.808712"},{"key":"49_CR3","unstructured":"Buck, D., Rau, A.: On modelling guidelines: Flowchart patterns for Stateflow. Softwaretechnik-Trends 21(2) (2001)"},{"key":"49_CR4","doi-asserted-by":"crossref","unstructured":"Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating discrete-time Simulink to Lustre. In: 3rd International ACM Conference on Embedded Software, Lecture Notes in Computer Science, vol. 2855, pp. 84\u201399. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45212-6_7"},{"key":"49_CR5","unstructured":"Ford: Structured analysis and design using Matlab\/Simulink\/Stateflow\u2014modeling style guidelines. Technical. report, Ford Motor Company (1999). http:\/\/vehicle.me.berkeley.edu\/mobies\/papers\/stylev242.pdf. Available at http:\/\/vehicle.me.berkeley.edu\/mobies\/papers\/stylev242.pdf"},{"issue":"1","key":"49_CR6","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S1567-8326(01)00012-1","volume":"51","author":"S. Gnesi","year":"2002","unstructured":"Gnesi S., Latella D. and Massink M. (2002). Modular semantics for a UML Statechart diagrams kernel and its extension to Multicharts and branching time model checking. J. Logic Algeb. Program. 51(1): 43\u201375","journal-title":"J. Logic Algeb. Program."},{"key":"49_CR7","doi-asserted-by":"crossref","unstructured":"Hamon, G.: A denotational semantics for Stateflow. In: EMSOFT 2005: Proceedings of the 5th ACM Workshop on Embedded Software, pp. 164\u2013172. Association for Computing Machinery, Jersey City, NJ (2005)","DOI":"10.1145\/1086228.1086260"},{"key":"49_CR8","doi-asserted-by":"crossref","unstructured":"Hamon, G., de Moura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods, pp. 261\u2013270. IEEE Computer Society, Beijing, China (2004)","DOI":"10.1109\/SEFM.2004.1347530"},{"key":"49_CR9","doi-asserted-by":"crossref","unstructured":"Hamon, G., de Moura, L., Rushby, J.: Automated test generation with SAL. Technical note, Computer Science Laboratory, SRI International, Menlo Park, CA Available at http:\/\/www.csl.sri.com\/users\/rushby\/abstracts\/sal-atg (2005)","DOI":"10.1007\/978-3-540-27813-9_45"},{"issue":"3","key":"49_CR10","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel D. (1987). Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3): 231\u2013274","journal-title":"Sci. Comput. Program."},{"key":"49_CR11","doi-asserted-by":"crossref","unstructured":"L\u00fcttgen, G., von der Beeck, M., Cleaveland, R.: A compositional approach to Statecharts semantics. In: Rosenblum, D., (ed.) 8th International ACM Symposium on Foundations of Software Engineering, pp. 120\u2013129. San Diego, Ca (2000)","DOI":"10.1145\/355045.355062"},{"key":"49_CR12","unstructured":"The Mathworks: Stateflow and Stateflow Coder, User\u2019s Guide, release 13sp1 edn. (2003). Available at http:\/\/www.mathworks. com\/access\/helpdesk\/help\/pdf_doc\/stateflow\/sf_ug.pdf"},{"key":"49_CR13","doi-asserted-by":"crossref","unstructured":"Mikk, E., Lakhnech, Y., Petersohn, C., Siegel, M.: On formal semantics of Statecharts as supported by Statemate. In: 2nd BCS-FACS Northern Formal Methods Workshop. BCS-EWIC (1997)","DOI":"10.14236\/ewic\/FA1997.12"},{"key":"49_CR14","doi-asserted-by":"crossref","unstructured":"de Moura, L, Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.(eds.) Computer-aided verification, CAV \u20192004, Lecture Notes in Computer Science, vol. 3114, pp. 496\u2013500. Springer, Boston, MA SAL home page: http:\/\/sal.csl.sri.com\/ (2004)","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"49_CR15","unstructured":"Plotkin, G.: A structural approach to operational semantics. Technical Report DAIMI-FN-19, Aarhus University (1981)"},{"key":"49_CR16","doi-asserted-by":"crossref","unstructured":"Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a \u201csafe\u201d subset of Simulink\/Stateflow into Lustre. In: EMSOFT 2004: Proceedings of the Fourth ACM Workshop on Embedded Software, pp. 259\u2013268. Pisa, Italy (2004)","DOI":"10.1145\/1017753.1017795"},{"key":"49_CR17","doi-asserted-by":"crossref","unstructured":"Strachey, C., Wadsworth, C.P.: Continuations: A mathematical semantics for handling full jumps. Higher-Order Symbolic Comput. 13, 135\u2013152 (2000), Originally published 1974","DOI":"10.1023\/A:1010026413531"},{"issue":"1","key":"49_CR18","first-page":"29","volume":"91","author":"A. Tiwari","year":"2003","unstructured":"Tiwari A., Shankar N. and Rushby J. (2003). Invisible formal methods for embedded control systems. In:Proceedings of the IEEE 91(1): 29\u201339","journal-title":"In:Proceedings of the IEEE"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0049-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-007-0049-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0049-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T16:18:42Z","timestamp":1683994722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-007-0049-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,31]]},"references-count":18,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2007,10,6]]}},"alternative-id":["49"],"URL":"https:\/\/doi.org\/10.1007\/s10009-007-0049-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7,31]]}}}