{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:59:54Z","timestamp":1770289194901,"version":"3.49.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,6,12]],"date-time":"2013-06-12T00:00:00Z","timestamp":1370995200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-013-0330-z","type":"journal-article","created":{"date-parts":[[2013,6,11]],"date-time":"2013-06-11T13:19:00Z","timestamp":1370956740000},"page":"343-363","source":"Crossref","is-referenced-by-count":17,"title":["Formal verification and validation of embedded systems: the UML-based MADES approach"],"prefix":"10.1007","volume":"14","author":[{"given":"Luciano","family":"Baresi","sequence":"first","affiliation":[]},{"given":"Gundula","family":"Blohm","sequence":"additional","affiliation":[]},{"given":"Dimitrios S.","family":"Kolovos","sequence":"additional","affiliation":[]},{"given":"Nicholas","family":"Matragkas","sequence":"additional","affiliation":[]},{"given":"Alfredo","family":"Motta","sequence":"additional","affiliation":[]},{"given":"Richard F.","family":"Paige","sequence":"additional","affiliation":[]},{"given":"Alek","family":"Radjenovic","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,6,12]]},"reference":[{"key":"330_CR1","unstructured":"Andersson, P., H\u00f6st, M., Bergstr\u00f6m, M.: UML to SystemC transformation in the MARTES project. In: Proceedings of the Work in Progress Session at Euromicro SEAA\/DSD (2006)"},{"key":"330_CR2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, C., Mallet, F., de Simone, R.: Modeling time(s). In: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science, vol. 4735, pp. 559\u2013573 (2007)","DOI":"10.1007\/978-3-540-75209-7_38"},{"key":"330_CR3","unstructured":"Bagnato, A., Andrey Sadovykh, E.B., Matragkas, N., Rossi, M., Baresi, L., Morzenti, A., Motta, A., Crippa, M.C., Genolini, S., Audsley, N.C., Gray, I., Indrusiak, L.S., Kolovos, D., Paige, R.: D1.7 mades final approach guide. Technical report, MADES Consortium (2012)"},{"key":"330_CR4","unstructured":"Bagnato, A., Sadovykh, A., Paige, R.F., Kolovos, D.S., Baresi, L., Morzenti, A., Rossi, M.: MADES: embedded systems engineering approach in the avionics domain. In: 1st Workshop on Hands-on Platforms and Tools for Model-Based Engineering of Embedded Systems (HoPES), p. 5 (2010)"},{"key":"330_CR5","doi-asserted-by":"crossref","unstructured":"Baresi, L., Ferretti, G., Leva, A., Rossi, M.: Flexible logic-based co-simulation of modelica models. In: IEEE International Conference on Industrial Informatics (INDIN), pp. 635\u2013640 (2012)","DOI":"10.1109\/INDIN.2012.6301223"},{"key":"330_CR6","doi-asserted-by":"crossref","unstructured":"Baresi, L., Morzenti, A., Motta, A., Rossi, M.: From interaction overview diagrams to temporal logic. In: MoDELS Workshops. Lecture Notes in Computer Science, vol. 6627, pp. 90\u2013104 (2010)","DOI":"10.1007\/978-3-642-21210-9_9"},{"key":"330_CR7","doi-asserted-by":"crossref","unstructured":"Baresi, L., Morzenti, A., Motta, A., Rossi, M.: Towards the UML-based formal verification of timed systems. In: Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol. 6957, pp. 267\u2013286 (2012)","DOI":"10.1007\/978-3-642-25271-6_14"},{"key":"330_CR8","doi-asserted-by":"crossref","unstructured":"Baresi, L., Orso, A., Pezz\u00e8, M.: Introducing formal specification methods in industrial practice. In: Proceedings of the 19th International Conference on Software Engineering (ICSE), pp. 56\u201366 (1997)","DOI":"10.1145\/253228.253241"},{"key":"330_CR9","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME), pp. 43\u201350 (2010)","DOI":"10.1109\/TIME.2010.21"},{"key":"330_CR10","unstructured":"Blohm, G., Bagnato, A.: D1.1 requirements specification. Tech. rep., MADES Consortium (2010). Available from MADES website. http:\/\/www.mades-project.org"},{"key":"330_CR11","unstructured":"Blohm, G., Eren, E., Bagnato, A., Bernardi, F.: D5.3 final evaluation report. Technical report, MADES Consortium (2012)"},{"key":"330_CR12","doi-asserted-by":"crossref","unstructured":"Burmester, S., Giese, H., Hirsch, M., Schilling, D., Tichy, M.: The fujaba real-time tool suite: model-driven development of safety-critical, real-time systems. In: Proceedings of the 27th International Conference on Software Engineering (ICSE), pp. 670\u2013671 (2005)","DOI":"10.1145\/1062455.1062601"},{"issue":"1","key":"330_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1921532.1921561","volume":"36","author":"C Choppy","year":"2011","unstructured":"Choppy, C., Klai, K., Zidani, H.: Formal verification of uml state diagrams: a petri net based approach. SIGSOFT Softw. Eng. Notes 36(1), 1\u20138 (2011)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"1","key":"330_CR14","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1145\/295558.295566","volume":"8","author":"E Ciapessoni","year":"1999","unstructured":"Ciapessoni, E., Coen-Porisini, A., Crivelli, E., Mandrioli, D., Mirandola, P., Morzenti, A.: From formal models to formally-based methods: an industrial experience. ACM Trans. Softw. Eng. Methodol. 8(1), 79\u2013113 (1999)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"330_CR15","doi-asserted-by":"crossref","unstructured":"Csert\u00e1n, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varr\u00f3, D.: VIATRA\u2014visual automated transformations for formal verification and validation of UML models. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering, pp. 267\u2013270 (2002)","DOI":"10.1109\/ASE.2002.1115027"},{"key":"330_CR16","unstructured":"Diethers, K., Huhn, M.: Vooduu: Verification of object-oriented designs using uppaal. In: Proceedings of TACAS. Lecture Notes in Computer Science, vol. 2988, pp. 139\u2013143 (2004). http:\/\/link.springer.com\/chapter\/10.1007%2F978-3-540-24730-2_10"},{"key":"330_CR17","doi-asserted-by":"crossref","unstructured":"Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: An overview of RoZ: a tool for integrating UML and Z specifications. In: Wangler B., Bergman L. (eds.) Advanced Information Systems Engineering. Lecture Notes in Computer Science, vol. 1789, pp. 417\u2013430 (2000)","DOI":"10.1007\/3-540-45140-4_28"},{"key":"330_CR18","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/j.scico.2008.09.001","volume":"74","author":"R Eshuis","year":"2009","unstructured":"Eshuis, R.: Reconciling statechart semantics. Sci. Comput. Programm. 74, 65\u201399 (2009)","journal-title":"Sci. Comput. Programm."},{"key":"330_CR19","unstructured":"Evans, A., France, R.B., Grant, E.S.: Towards formal reasoning with UML models (1999)"},{"key":"330_CR20","unstructured":"Falleri, J.R., Huchard, M., Nebut, C.: Towards a traceability framework for model transformations in Kermeta. In: ECMDA Traceability Workshop (ECMDA-TW\u201906) (2006)"},{"key":"330_CR21","doi-asserted-by":"crossref","DOI":"10.1109\/9780470545669","volume-title":"Principles of Object-Oriented Modeling and Simulation with Modelica 2.1","author":"PA Fritzson","year":"2004","unstructured":"Fritzson, P.A.: Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Wiley, London (2004)"},{"key":"330_CR22","doi-asserted-by":"crossref","unstructured":"Gray, I., Audsley, N.C.: Exposing non-standard architectures to embedded software using compile-time virtualisation. In: Proceedings of the 2009 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES), pp. 147\u2013156 (2009)","DOI":"10.1145\/1629395.1629417"},{"issue":"3","key":"330_CR23","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1109\/52.896248","volume":"17","author":"CA Gunter","year":"2000","unstructured":"Gunter, C.A., Gunter, E.L., Jackson, M., Zave, P.: A reference model for requirements and specifications. Softw. IEEE 17(3), 37\u201343 (2000)","journal-title":"Softw. IEEE"},{"key":"330_CR24","doi-asserted-by":"crossref","unstructured":"Hammal, Y.: A formal semantics of UML statecharts by means of timed petri nets. In: Proceedings of FORTE. Lecture Notes in Computer Science, vol. 3731, pp. 38\u201352 (2005)","DOI":"10.1007\/11562436_5"},{"key":"330_CR25","unstructured":"Jackson, D.: Lightweight formal methods. In: FME 2001: Formal Methods for Increasing Software Productivity. Lecture Notes in Computer Science, vol. 2021, pp. 1\u20131 (2001). http:\/\/link.springer.com\/chapter\/10.1007%2F3-540-45251-6_1"},{"key":"330_CR26","unstructured":"Jouault, F., Allilaire, F., B\u00e9zivin, J., Kurtev, I., Valduriez, P.: ATL: a QVT-like transformation language. In: Companion to the 21st ACM SIGPLAN Symposium on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA\u201906, pp. 719\u2013720 (2006)"},{"key":"330_CR27","unstructured":"Kolovos, D.S., Paige, R., Rose, L., Polack, F.: The Epsilon Book. York, UK, Technical report, The University of York (2010)"},{"key":"330_CR28","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.entcs.2009.09.064","volume":"254","author":"V Lima","year":"2009","unstructured":"Lima, V., Talhi, C., Mouheb, D., Debbabi, M., Wang, L., Pourzandi, M.: Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. Electron. Notes Theor. Comput. Sci. 254, 143\u2013160 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"330_CR29","unstructured":"MADES: Model-based methods and tools for Avionics and surveillance embeddeD SystEmS (2012). http:\/\/www.mades-project.org\/"},{"key":"330_CR30","unstructured":"Nielsen, B.: Quasimodo\u2014quantitative system properties in model-driven-design of embedded systems (2007). http:\/\/www.quasimodo.aau.dk"},{"key":"330_CR31","unstructured":"Object Management Group: Semantics of a foundational subset for executable UML models (fUML). Technical report, OMG (2011). Formal\/2011-02-01"},{"key":"330_CR32","unstructured":"OMG: UML Profile for MARTE: Modeling and Analysis of Real-time Embedded Systems. Technical report, November, OMG (2009)"},{"key":"330_CR33","unstructured":"OMG: Unified Modeling Language\u2014Infrastructure. Technical report, May, OMG (2010). http:\/\/www.omg.org\/spec\/UML\/2.3\/Infrastructure\/PDF\/"},{"key":"330_CR34","unstructured":"\u00c9ric, P., Atitallah, R.B., Marquet, P., Meftali, S., Niar, S., Etien, A., Dekeyser, J.-L., Boulet, P.: Gaspard2: from MARTE to SystemC Simulation. In: Proceeedings of the DATE\u201908 Workshop on Modeling and Analysis of Real-Time and Embedded Systems with the MARTE UML Profile (2008). www2.linfl.fr\/marteworkshop\/proceedingsMarteWS08.pdf"},{"key":"330_CR35","doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. Softw. Eng. Methodol. (2012, in press)","DOI":"10.1145\/2491509.2491514"},{"key":"330_CR36","doi-asserted-by":"crossref","unstructured":"Radjenovic, A., Matragkas, N.D., Paige, R.F., Rossi, M., Motta, A., Baresi, L., Kolovos, D.S.: MADES: a tool chain for automated verification of UML models of embedded systems. In: Modelling Foundations and Applications. Lecture Notes in Computer Science, vol. 7349, pp. 340\u2013351 (2012)","DOI":"10.1007\/978-3-642-31491-9_26"},{"key":"330_CR37","doi-asserted-by":"crossref","unstructured":"Rose, L.M., Paige, R.F., Kolovos, D.S., Polack, F.A.: The epsilon generation language. In: Proceedings of the 4th European Conference on Model Driven Architecture: Foundations and Applications (ECMDA-FA), pp. 1\u201316 (2008)","DOI":"10.1007\/978-3-540-69100-6_1"},{"key":"330_CR38","unstructured":"Saldhana, J.A., Shatz, S.M.: UML diagrams to object petri net models: an approach for modeling and analysis. In: Proceedings of SEKE 2000, pp. 103\u2013110 (2000)"},{"key":"330_CR39","doi-asserted-by":"crossref","unstructured":"Schamai, W., Fritzson, P., Paredis, C., Pop, A.: Towards unified system modeling and simulation with modelicaml: modeling of executable behavior using graphical notations. In: Proceedings of the 7th International Modelica Conference, pp. 612\u2013621 (2009)","DOI":"10.3384\/ecp09430081"},{"key":"330_CR40","doi-asserted-by":"crossref","unstructured":"Staines, T.: Intuitive mapping of UML 2 activity diagrams into fundamental modeling concept petri net diagrams and colored petri nets. In: IEEE International Conference and Workshop on the Engineering of Computer Based Systems, pp. 191\u2013200 (2008)","DOI":"10.1109\/ECBS.2008.12"},{"key":"330_CR41","unstructured":"St\u00f6rrle, H., Hausmann, J.H.: Towards a Formal Semantics of UML 2.0 Activities (2005)"},{"key":"330_CR42","unstructured":"Than, X., Miao, H., Liu, L.: Formalizing the semantics of UML statecharts with Z. In: The Fourth International Conference on Computer and Information Technology (CIT), pp. 1116\u20131121 (2004)"},{"key":"330_CR43","unstructured":"The Eclipse Foundation: Eclipse Modeling Framework (EMF) (2012). http:\/\/www.eclipse.org\/modeling\/emf\/"},{"key":"330_CR44","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/j.entcs.2010.05.013","volume":"263","author":"JR Williams","year":"2010","unstructured":"Williams, J.R., Polack, F.A.C.: Automated formalisation for verification of diagrammatic models. Electr. Notes Theor. Comput. Sci. 263, 211\u2013226 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"330_CR45","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009). http:\/\/dl.acm.org\/citation.cfm?id=1592436"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0330-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0330-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0330-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,15]],"date-time":"2019-07-15T04:34:04Z","timestamp":1563165244000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0330-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,12]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["330"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0330-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,12]]}}}