{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T10:26:17Z","timestamp":1791109577202,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642415326","type":"print"},{"value":"9783642415333","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41533-3_20","type":"book-chapter","created":{"date-parts":[[2013,9,19]],"date-time":"2013-09-19T11:40:59Z","timestamp":1379590859000},"page":"320-335","source":"Crossref","is-referenced-by-count":3,"title":["Behavioural Verification in Embedded Software, from Model to Source Code"],"prefix":"10.1007","author":[{"given":"Anthony Fernandes","family":"Pires","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Polacsek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Virginie","family":"Wiels","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"St\u00e9phane","family":"Duprat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-642-05089-3_34","volume-title":"FM 2009: Formal Methods","author":"J. Souyris","year":"2009","unstructured":"Souyris, J., Wiels, V., Delmas, D., Delseny, H.: Formal verification of avionics software products. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 532\u2013546. Springer, Heidelberg (2009)"},{"issue":"10","key":"20_CR2","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"7","key":"20_CR3","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/S0920-5489(98)00020-8","volume":"19","author":"R. France","year":"1998","unstructured":"France, R., Evans, A., Lano, K., Rumpe, B.: The uml as a formal modeling notation. Comput. Stand. Interfaces\u00a019(7), 325\u2013334 (1998)","journal-title":"Comput. Stand. Interfaces"},{"key":"20_CR4","unstructured":"Fernandes Pires, A., Duprat, S., Faure, T., Besseyre, C., Beringuier, J., Rolland, J.F.: Use of modelling methods and tools in an industrial embedded system project: works and feedback. In: ERTS, France (2012)"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming\u00a019(2), 87\u2013152 (1992)","journal-title":"Science of Computer Programming"},{"key":"20_CR6","unstructured":"Gomez, M.: Embedded state machine implementation. Embedded Systems Programming\u00a041 (2000)"},{"key":"20_CR7","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL Version 1.6. (2012)"},{"issue":"8","key":"20_CR8","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"20_CR9","unstructured":"Duprat, S., Gaufillet, P., Moya Lamiel, V., Passarello, F.: Formal verification of sam state machine implementation. In: ERTS, France (2010)"},{"key":"20_CR10","unstructured":"Stouls, N., Prevosto, V.: Aora\u00ef Plug-in Tutorial"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Jobredeaux, R., Wang, T., Feron, E.: Autocoding control software with proofs i: Annotation translation. In: 2011 IEEE\/AIAA 30th Digital Avionics Systems Conference (DASC), pp. 7C1-1\u20137C1-13 (October 2011)","DOI":"10.1109\/DASC.2011.6096122"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language lustre. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","DOI":"10.1109\/5.97300"},{"key":"20_CR13","unstructured":"Crane, M.L., Dingel, J.: On the semantics of uml state machines: Categorization and comparision. In: Technical Report 2005-501, School of Computing, Queen\u2019s University (2005)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-46428-X_10","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Reggio","year":"2000","unstructured":"Reggio, G., Astesiano, E., Choppy, C., Hussmann, H.: Analysing uml active classes and associated state machines - a lightweight formal approach. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 127\u2013146. Springer, Heidelberg (2000)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-44518-8_13","volume-title":"Abstract State Machines - Theory and Applications","author":"E. B\u00f6rger","year":"2000","unstructured":"B\u00f6rger, E., Cavarra, A., Riccobene, E.: Modeling the dynamics of uml state machines. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol.\u00a01912, pp. 223\u2013241. Springer, Heidelberg (2000)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-45832-8_28","volume-title":"Graph Transformation","author":"D. Varr\u00f3","year":"2002","unstructured":"Varr\u00f3, D.: A formal semantics of uml statecharts by model transition systems. In: Corradini, A., Ehrig, H., Kreowski, H.J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol.\u00a02505, pp. 378\u2013392. Springer, Heidelberg (2002)"},{"key":"20_CR17","unstructured":"Gogolla, M., Presicce, F.P.: State diagrams in uml: A formal semantics using graph transformations - or diagrams are nice, but graphs are worth their price. In: University of Munich, pp. 55\u201372 (1998)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-45397-0_9","volume-title":"Concurrent Object-Oriented Programming and Petri Nets","author":"L. Baresi","year":"2001","unstructured":"Baresi, L., Pezz\u00e8, M.: On formalizing uml with high-level petri nets. In: Agha, G., De Cindio, F., Rozenberg, G. (eds.) APN 2001. LNCS, vol.\u00a02001, pp. 276\u2013304. Springer, Heidelberg (2001)"},{"key":"20_CR19","unstructured":"Aredo, D.B.: Semantics of uml statecharts in pvs. In: Proc. of the 12th Nordic Workshop on Programming Theory (NWPT 2000) (2001)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-46852-8_31","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"J. Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.P.: Formalising uml state machines for model checking. In: France, R.B. (ed.) UML 1999. LNCS, vol.\u00a01723, pp. 430\u2013444. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Model-Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41533-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T07:37:17Z","timestamp":1558078637000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41533-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415326","9783642415333"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41533-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}