{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T10:18:27Z","timestamp":1790504307665,"version":"4.1.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,5,3]],"date-time":"2018-05-03T00:00:00Z","timestamp":1525305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10270-018-0676-3","type":"journal-article","created":{"date-parts":[[2018,5,3]],"date-time":"2018-05-03T01:21:10Z","timestamp":1525310470000},"page":"837-863","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["A method for testing and validating executable statechart models"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3636-5020","authenticated-orcid":false,"given":"Tom","family":"Mens","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"Decan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4957-9194","authenticated-orcid":false,"given":"Nikolaos I.","family":"Spanoudakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,5,3]]},"reference":[{"key":"676_CR1","unstructured":"Aravantinos, V., Voss, S., Teufl, S., H\u00f6lzl, F., Sch\u00e4tz, B.: AutoFOCUS 3: tooling concepts for seamless, model-based development of embedded systems. In: International Workshop on Model-Based Architecting of Cyber-Physical and Embedded Systems and International Workshop on UML Consistency Rules, Volume 1508 of CEUR Workshop Proceedings, pp. 19\u201326. CEUR-WS.org (2015)"},{"key":"676_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"676_CR3","volume-title":"Test-Driven Development by Example","author":"K Beck","year":"2002","unstructured":"Beck, K.: Test-Driven Development by Example. Addison-Wesley, Reading (2002)"},{"key":"676_CR4","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: International Conference Computer Aided Verification (CAV), pp. 363\u2013367. Springer (2001)","DOI":"10.1007\/3-540-44585-4_33"},{"key":"676_CR5","doi-asserted-by":"crossref","unstructured":"Bunse, C., Klingert, S., Schulze, T.: Greenslas: supporting energy-efficiency through contracts. In: International Workshop on Energy Efficient Data Centers, pp. 54\u201368. Springer (2012)","DOI":"10.1007\/978-3-642-33645-4_6"},{"key":"676_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2014.03.023","volume":"93","author":"J Cabot","year":"2014","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: On the verification of UML\/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1\u201323 (2014)","journal-title":"J. Syst. Softw."},{"key":"676_CR7","doi-asserted-by":"crossref","unstructured":"Cariou, E., Ballagny, C., Feugas, A., Barbier, F.: Contracts for model execution verification. In: European Conference Modelling Foundations and Applications (ECMFA), Volume 6698 of Lecturer Notes in Computer Science, pp. 3\u201318. Springer (2011)","DOI":"10.1007\/978-3-642-21470-7_2"},{"key":"676_CR8","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program."},{"key":"676_CR9","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: A language framework for expressing checkable properties of dynamic software. In: International SPIN Model Checking and Software Verification Workshop, Volume 1885 of Lecturer Notes in Computer Science, pp. 205\u2013223. Springer (2000)","DOI":"10.1007\/10722468_13"},{"issue":"1","key":"676_CR10","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1504\/IJAOSE.2007.013266","volume":"1","author":"M Cossentino","year":"2007","unstructured":"Cossentino, M., Gaglio, S., Garro, A., Seidita, V.: Method fragments for agent design methodologies: from standardisation to research. Int. J. Agent Oriented Softw. Eng. 1(1), 91\u2013121 (2007)","journal-title":"Int. J. Agent Oriented Softw. Eng."},{"key":"676_CR11","doi-asserted-by":"crossref","unstructured":"Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: International Conference on Financial Cryptography and Data Security, pp. 79\u201394. Springer (2016)","DOI":"10.1007\/978-3-662-53357-4_6"},{"key":"676_CR12","doi-asserted-by":"crossref","unstructured":"Dietrich, I., Dressler, F., Dulz, W., German, R.: Validating UML simulation models with model-level unit tests. In: International Conference Simulation Tools and Techniques (SIMUTools) (2010)","DOI":"10.4108\/ICST.SIMUTOOLS2010.8629"},{"key":"676_CR13","volume-title":"Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns","author":"BP Douglas","year":"1999","unstructured":"Douglas, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, Reading (1999)"},{"key":"676_CR14","doi-asserted-by":"crossref","unstructured":"Drusinsky, D.: Semantics and runtime monitoring of TLCharts: statechart automata with temporal logic conditioned transitions. In: Proceedings of the Fourth Workshop on Runtime Verification (RV 2004), Electronic Notes in Theoretical Computer Science, Volume 113, pp. 3\u201321 (2005)","DOI":"10.1016\/j.entcs.2004.01.025"},{"key":"676_CR15","volume-title":"Modeling and Verification Using UML Statecharts","author":"D Drusinsky","year":"2006","unstructured":"Drusinsky, D.: Modeling and Verification Using UML Statecharts. Elsevier Science, Amsterdam (2006)"},{"key":"676_CR16","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"issue":"1\u20133","key":"676_CR17","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"676_CR18","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s00766-010-0102-z","volume":"15","author":"S Esmaeilsabzali","year":"2010","unstructured":"Esmaeilsabzali, S., Day, N.A., Atlee, J.M., Niu, J.: Deconstructing the semantics of big-step modelling languages. Requir. Eng. 15(2), 235\u2013265 (2010)","journal-title":"Requir. Eng."},{"key":"676_CR19","doi-asserted-by":"crossref","unstructured":"Estler, H., Furia, C.A., Nordio, M., Piccioni, M., Meyer, B.: Contracts in practice. In: International Symposium on Formal Methods (FM), Volume 8442 of Lecturer Notes in Computer Science, pp. 230\u2013246. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_17"},{"key":"676_CR20","doi-asserted-by":"crossref","unstructured":"Fabbri, S.C.P.F., Maldonado, J.C., Sugeta, T., Masiero, P.C.: Mutation testing applied to validate specifications based on statecharts. In: International Symposium on Software Reliability Engineering (ISSRE), pp. 210\u2013219. IEEE Computer Society (1999)","DOI":"10.1109\/ISSRE.1999.809326"},{"key":"676_CR21","first-page":"141","volume":"34","author":"Y Falcone","year":"2013","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Dependable Softw. Syst. 34, 141\u2013175 (2013)","journal-title":"Eng. Dependable Softw. Syst."},{"key":"676_CR22","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Latella, D., Massink M.: Model checking UML statechart diagrams using JACK. In: International Symposium on High-Assurance Systems Engineering (HASE), pp. 46\u201355. IEEE Computer Society (1999)","DOI":"10.1109\/HASE.1999.809474"},{"key":"676_CR23","doi-asserted-by":"crossref","unstructured":"Gogolla, M., Hamann, L., Hilken, F., Sedlmeier, M.: Modeling behavior with interaction diagrams in a UML and OCL tool. In: Behavior Modeling\u2014Foundations and Applications, BM-FA 2009\u20132014, Revised Selected Papers, Volume 6368 of Lecturer Notes in Computer Science, pp. 31\u201358. Springer (2015)","DOI":"10.1007\/978-3-319-21912-7_2"},{"issue":"1\u20133","key":"676_CR24","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.scico.2007.01.013","volume":"69","author":"M Gogolla","year":"2007","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1\u20133), 27\u201334 (2007)","journal-title":"Sci. Comput. Program."},{"key":"676_CR25","volume-title":"Designing Software Product Lines with UML: From Use Cases to Pattern-Based Software Architectures","author":"H Gomaa","year":"2004","unstructured":"Gomaa, H.: Designing Software Product Lines with UML: From Use Cases to Pattern-Based Software Architectures. Addison Wesley, Reading (2004)"},{"key":"676_CR26","doi-asserted-by":"crossref","unstructured":"Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: International Conference on Model Driven Engineering Languages and Systems, Volume 7590 of Lecturer Notes in Computer Science, pp. 235\u2013251. Springer (2012)","DOI":"10.1007\/978-3-642-33666-9_16"},{"issue":"5","key":"676_CR27","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1145\/42411.42414","volume":"31","author":"D Harel","year":"1988","unstructured":"Harel, D.: On visual formalisms. Commun. ACM 31(5), 514\u2013530 (1988)","journal-title":"Commun. ACM"},{"issue":"7","key":"676_CR28","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/2.596624","volume":"30","author":"D Harel","year":"1997","unstructured":"Harel, D., Gery, E.: Executable object modeling with statecharts. IEEE Comput. 30(7), 31\u201342 (1997)","journal-title":"IEEE Comput."},{"key":"676_CR29","volume-title":"The Rhapsody Semantics of Statecharts (or, on the Executable Core of the UML), Volume LNCS 3147","author":"D Harel","year":"2004","unstructured":"Harel, D., Kugler, H.: The Rhapsody Semantics of Statecharts (or, on the Executable Core of the UML), Volume LNCS 3147. Springer, Berlin (2004)"},{"issue":"4","key":"676_CR30","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"3","key":"676_CR31","first-page":"424","volume":"16","author":"B Henderson-Sellers","year":"2010","unstructured":"Henderson-Sellers, B., Ralyt\u00e9, J.: Situational method engineering: state-of-the-art review. J. Univers. Comput. Sci. 16(3), 424\u2013478 (2010)","journal-title":"J. Univers. Comput. Sci."},{"key":"676_CR32","doi-asserted-by":"crossref","unstructured":"Idelberger, F., Governatori, G., Riveret, R., Sartor, G.: Evaluation of logic-based smart contracts for blockchain systems. In: International Symposium on Rules and Rule Markup Languages for the Semantic Web, pp. 167\u2013183. Springer (2016)","DOI":"10.1007\/978-3-319-42019-6_11"},{"issue":"1","key":"676_CR33","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.entcs.2010.07.007","volume":"264","author":"I Lazar","year":"2010","unstructured":"Lazar, I., Motogna, S., Parv, B.: Behaviour-driven development of foundational UML components. Electron. Notes Theor. Comput. Sci. 264(1), 91\u2013105 (2010). (Int\u2019l Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA))","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"676_CR34","unstructured":"Leavens, G.T., Cheon, Y.: Design by Contract with JML. Technical report, Iowa State University (2006)"},{"issue":"5","key":"676_CR35","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Program. 78(5), 293\u2013303 (2009). (The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS\u201907))","journal-title":"J. Logic Algebr. Program."},{"key":"676_CR36","doi-asserted-by":"crossref","unstructured":"Magee, J.: Behavioral analysis of software architectures using LTSA. In: International Conference on Software Engineering, pp. 634\u2013637. ACM (1999)","DOI":"10.1145\/302405.302726"},{"key":"676_CR37","doi-asserted-by":"crossref","unstructured":"Meyer, B.: Contract-driven development. In: International Conference on Fundamental Approaches to Software Engineering (FASE), Volume 4422 of Lecturer Notes in Computer Science, p. 11. Springer (2007)","DOI":"10.1007\/978-3-540-71289-3_2"},{"issue":"10","key":"676_CR38","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \"design by contract\". IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"676_CR39","unstructured":"North, D.: Behavior modification: the evolution of behavior-driven development. Better Software (2006)"},{"key":"676_CR40","unstructured":"Object Management Group. Object Constraint Language, Version 2.4. OMG Document Number: formal\/2014-02-03. URL: http:\/\/www.omg.org\/spec\/OCL\/2.4 (2014)"},{"key":"676_CR41","unstructured":"Object Management Group. OMG Unified Modeling Language (OMG UML), Version 2.5. OMG Document Number: formal\/2015-03-01. URL: http:\/\/www.omg.org\/spec\/UML\/2.5 (2015)"},{"key":"676_CR42","unstructured":"OMG. Software and Systems Process Engineering Meta-Model Specification. Version 2.0. Technical Report OMG Document Number: Formal\/2008-04-01. Object Management Group (2008)"},{"issue":"5","key":"676_CR43","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1109\/TSE.2014.2312918","volume":"40","author":"Y Pei","year":"2014","unstructured":"Pei, Y., Furia, C.A., Nordio, M., Wei, Y., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. IEEE Trans. Soft. Eng. 40(5), 427\u2013449 (2014)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"676_CR44","doi-asserted-by":"publisher","DOI":"10.1201\/b16463","volume-title":"Practical UML Statecharts in C\/C++: Event-Driven Programming for Embedded Systems","author":"M Samek","year":"2008","unstructured":"Samek, M.: Practical UML Statecharts in C\/C++: Event-Driven Programming for Embedded Systems, 2nd edn. CRC Press, Boca Raton (2008)","edition":"2"},{"key":"676_CR45","doi-asserted-by":"crossref","unstructured":"Sen, K.: Concolic testing. In: International Conference on Automated Software Engineering, pp. 571\u2013572. ACM (2007)","DOI":"10.1145\/1321631.1321746"},{"key":"676_CR46","first-page":"32","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications, Volume 5253 of Lecture Notes in Computer Science","author":"N Spanoudakis","year":"2008","unstructured":"Spanoudakis, N., Moraitis, P.: The agent modeling language (AMOLA). In: Dochev, D., Pistore, M., Traverso, P. (eds.) Artificial Intelligence: Methodology, Systems, and Applications, Volume 5253 of Lecture Notes in Computer Science, pp. 32\u201344. Springer, Berlin (2008)"},{"key":"676_CR47","unstructured":"Syriani, E., Vangheluwe, H., Mannadiar, R., Hansen, C., Van\u00a0Mierlo, S., Ergin, H.: AToMPM: a web-based modeling environment. In: Joint Proceedings of MODELS\u201913 Invited Talks, Demonstration Session, Poster Session, and ACM Student Research Competition, Volume 1115, CEUR Workshop Proceedings (2013)"},{"key":"676_CR48","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-39250-4_21","volume-title":"RoboCup 2012: Robot Soccer World Cup XVI. Lecture Notes in Computer Science","author":"A Topalidou-Kyniazopoulou","year":"2013","unstructured":"Topalidou-Kyniazopoulou, A., Spanoudakis, N.I., Lagoudakis, M.G.: A CASE tool for robot behavior development. In: Chen, X., Stone, P., Sucar, L.E., Zant, T. (eds.) RoboCup 2012: Robot Soccer World Cup XVI. Lecture Notes in Computer Science, vol. 7500, pp. 225\u2013236. Springer, Berlin (2013)"},{"key":"676_CR49","doi-asserted-by":"crossref","unstructured":"Trakhtenbrot, M.: New mutations for evaluation of specification and implementation levels of adequacy in testing of statecharts models. In: Testing: Academic and Industrial Conference Practice and Research Techniques (MUTATION), pp. 151\u2013160 (2007)","DOI":"10.1109\/TAICPART.2007.4344119"},{"key":"676_CR50","unstructured":"Wynne, M., Hellesoy, A.: The Cucumber Book: Behaviour-Driven Development for Testers and Developers. Pragmatic Bookshelf. ISBN: 978-1-93435-680-7. https:\/\/pragprog.com\/book\/hwcuc\/the-cucumber-book (2012)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-018-0676-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-018-0676-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-018-0676-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T02:19:55Z","timestamp":1751595595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-018-0676-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,3]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["676"],"URL":"https:\/\/doi.org\/10.1007\/s10270-018-0676-3","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,3]]},"assertion":[{"value":"29 August 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 April 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}