{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:41:49Z","timestamp":1725896509916},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314902"},{"type":"electronic","value":"9783642314919"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31491-9_26","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T21:28:19Z","timestamp":1340314099000},"page":"340-351","source":"Crossref","is-referenced-by-count":2,"title":["MADES: A Tool Chain for Automated Verification of UML Models of Embedded Systems"],"prefix":"10.1007","author":[{"given":"Alek","family":"Radjenovic","sequence":"first","affiliation":[]},{"given":"Nicholas","family":"Matragkas","sequence":"additional","affiliation":[]},{"given":"Richard F.","family":"Paige","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]},{"given":"Alfredo","family":"Motta","sequence":"additional","affiliation":[]},{"given":"Luciano","family":"Baresi","sequence":"additional","affiliation":[]},{"given":"Dimitrios S.","family":"Kolovos","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Audsley, N.C., Gray, I., Indrusiak, L.S., Kolovos, D., Matragkas, N., Paige, R.: Model-based development of embedded systems - the MADES approach. In: 2nd Workshop on Model Based Engineering for Embedded Systems Design (MBED 2011), pp. 1\u20134 (2011)"},{"key":"26_CR2","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 2010), p. 5 (2010)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-25271-6_14","volume-title":"Formal Methods for Components and Objects","author":"L. Baresi","year":"2011","unstructured":"Baresi, L., Morzenti, A., Motta, A., Rossi, M.: Towards the UML-Based Formal Verification of Timed Systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 267\u2013286. Springer, Heidelberg (2011)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Bernardi, S., Donatelli, S., Merseguer, J.: From UML Sequence Diagrams and Statecharts to analysable Petri Net models. In: 3rd International Workshop on Software and Performance, pp. 35\u201345 (2002)","DOI":"10.1145\/584374.584376"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-78743-3_8","volume-title":"Fundamental Approaches to Software Engineering","author":"A.D. Brucker","year":"2008","unstructured":"Brucker, A.D., Wolff, B.: HOL-OCL: A Formal Proof Environment for uml\/ocl. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 97\u2013100. Springer, Heidelberg (2008)"},{"key":"26_CR6","unstructured":"Cabot, J., Clariso, R.: UML\/OCL Verification In Practice. In: ChaMDE Workshop (MODELS 2008), pp. 31\u201335 (2008)"},{"key":"26_CR7","first-page":"547","volume-title":"22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2007)","author":"J. Cabot","year":"2007","unstructured":"Cabot, J., Clariso, R., Riera, D.: UMLtoCSP: A Tool for the Formal Verification of UML\/OCL Models Using Constraint Programming. In: 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2007), pp. 547\u2013548. ACM, New York (2007)"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Cabot, J., Clariso, R., Riera, D.: Verification of UML\/OCL Class Diagrams using Constraint Programming. In: IEEE International Conference on Software Testing Verification and Validation Workshop (ICSTW 2008), IEEE (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"26_CR9","volume-title":"Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logics of Programs, Springer, Heidelberg (1981)"},{"issue":"3","key":"26_CR10","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1147\/sj.453.0621","volume":"45","author":"K. Czarnecki","year":"2006","unstructured":"Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Systems Journal\u00a045(3), 621\u2013645 (2006)","journal-title":"IBM Systems Journal"},{"key":"26_CR11","unstructured":"The Eclipse Foundation. Eclipse Modeling Framework (EMF) (2012), \n                  \n                    http:\/\/www.eclipse.org\/modeling\/emf\/"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-02949-3_8","volume-title":"Tests and Proofs","author":"M. Gogolla","year":"2009","unstructured":"Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, Independence and Consequences in UML and OCL Models. In: Dubois, C. (ed.) TAP 2009. LNCS, vol.\u00a05668, pp. 90\u2013104. Springer, Heidelberg (2009)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-540-24732-6_6","volume-title":"Model Checking Software","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J., Joshi, R.: Model-Driven Software Verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 76\u201391. Springer, Heidelberg (2004)"},{"issue":"4","key":"26_CR14","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C. Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearn, P., Woodcock, J.: Verified software: a grand challenge. Computer\u00a039(4), 93\u201395 (2006)","journal-title":"Computer"},{"key":"26_CR15","unstructured":"Kolovos, D.S., Paige, R., Rose, L., Polack, F.: The Epsilon Book. Technical report, The University of York, York, UK (2010)"},{"key":"26_CR16","unstructured":"MADES. Model-based methods and tools for Avionics and surveillance embeddeD SystEmS (2012), \n                  \n                    http:\/\/www.mades-project.org\/"},{"key":"26_CR17","unstructured":"MIT. alloy (2012), \n                  \n                    http:\/\/alloy.mit.edu\/alloy\/"},{"key":"26_CR18","unstructured":"OMG. OMG Systems Modeling Language (OMG SysML), v1.2. Technical report, OMG (2007)"},{"key":"26_CR19","unstructured":"OMG. UML Profile for MARTE : Modeling and Analysis of Real-Time Embedded Systems. Technical Report November, OMG (2009)"},{"key":"26_CR20","unstructured":"OMG. Unified Modeling Language - Infrastructure. Technical Report May, OMG (2010)"},{"key":"26_CR21","unstructured":"OMG. Unified Modeling Language - Superstructure. Technical Report May, OMG (2010)"},{"key":"26_CR22","unstructured":"OMG. MOF 2 XMI Mapping Specification. Technical report, OMG (2011)"},{"key":"26_CR23","unstructured":"OMG. OMG Object Constraint Language ( OCL ) v2.3.1. Technical Report January, OMG (2012)"},{"key":"26_CR24","first-page":"312","volume-title":"Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE 2007","author":"M. Pradella","year":"2007","unstructured":"Pradella, M., Morzenti, A., Pietro, P.S.: The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In: Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE 2007, pp. 312\u2013320. ACM, New York (2007)"},{"key":"26_CR25","volume-title":"5th International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th International Symposium on Programming, Springer, Heidelberg (1982)"},{"issue":"2","key":"26_CR26","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/MC.2006.58","volume":"39","author":"D.C. Schmidt","year":"2006","unstructured":"Schmidt, D.C.: Model Driven Engineering. Computer\u00a039(2), 25\u201331 (2006)","journal-title":"Computer"},{"issue":"5","key":"26_CR27","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/MS.2003.1231146","volume":"20","author":"B. Selic","year":"2003","unstructured":"Selic, B.: The pragmatics of model-driven development. IEEE Software\u00a020(5), 19\u201325 (2003)","journal-title":"IEEE Software"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-21652-7_11","volume-title":"System Analysis and Modeling: About Models","author":"A. Shaikh","year":"2011","unstructured":"Shaikh, A., Wiil, U.K., Memon, N.: UOST: UML\/OCL Aggressive Slicing Technique for Efficient Verification of Models. In: Kraemer, F.A., Herrmann, P. (eds.) SAM 2010. LNCS, vol.\u00a06598, pp. 173\u2013192. Springer, Heidelberg (2011)"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL Models Using Boolean Satisfiability. In: Conference on Design, Automation and Test in Europe (DATE 2010). European Design and Automation Association, pp. 1341\u20131344 (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"26_CR30","unstructured":"SOFTEAM. Modelio (2012), \n                  \n                    http:\/\/modelio.org\/"},{"issue":"2","key":"26_CR31","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"M.H. Beek ter","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Science of Computer Programming\u00a076(2), 119\u2013135 (2011)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Modelling Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31491-9_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:03:32Z","timestamp":1620129812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31491-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314902","9783642314919"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31491-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}