{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T05:23:54Z","timestamp":1766381034790,"version":"3.40.5"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2023,4]]},"DOI":"10.1007\/s10270-022-01012-1","type":"journal-article","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T05:02:51Z","timestamp":1659762171000},"page":"733-749","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Dash: declarative behavioural modelling in Alloy with control state hierarchy"],"prefix":"10.1007","volume":"22","author":[{"given":"Jose","family":"Serna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1422-692X","authenticated-orcid":false,"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shahram","family":"Esmaeilsabzali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"issue":"2","key":"1012_CR1","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/MC.2006.58","volume":"39","author":"D Schmidt","year":"2006","unstructured":"Schmidt, D.: Guest editor\u2019s introduction: model-driven engineering. IEEE Comput. 39(2), 25\u201331 (2006)","journal-title":"IEEE Comput."},{"key":"1012_CR2","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019)","DOI":"10.1145\/3338843"},{"key":"1012_CR3","volume-title":"Software Abstractions","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions, 2nd edn. MIT Press, Cambridge (2012)","edition":"2"},{"issue":"3","key":"1012_CR4","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1016\/j.scico.2011.03.008","volume":"78","author":"MC Reynolds","year":"2013","unstructured":"Reynolds, M.C.: Modeling the java bytecode verifier. Sci. Comput. Program. 78(3), 327\u2013342 (2013)","journal-title":"Sci. Comput. Program."},{"issue":"12","key":"1012_CR5","doi-asserted-by":"publisher","first-page":"1144","DOI":"10.1109\/TSE.2017.2655056","volume":"43","author":"P Zave","year":"2017","unstructured":"Zave, P.: Reasoning about identifier spaces: How to make chord correct. IEEE Trans. Softw. Eng. 43(12), 1144\u20131156 (2017)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1012_CR6","doi-asserted-by":"crossref","unstructured":"Kang, E., Adepu, S., Jackson, D., Mathur, A.P.: Model-based security analysis of a water treatment system. In: IEEE\/ACM 2nd International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS), IEEE, pp. 22\u201328 (2016)","DOI":"10.1145\/2897035.2897041"},{"key":"1012_CR7","doi-asserted-by":"crossref","unstructured":"Svendsen, A., M\u00f8ller-Pedersen, B., Haugen, \u00d8., Endresen, J., Carlson, E.: Formalizing train control language: automating analysis of train stations. In: Comprail, pp. 245\u2013256 (2010)","DOI":"10.2495\/CR100241"},{"key":"1012_CR8","first-page":"117","volume-title":"Advances in Computers","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers, vol. 58, pp. 117\u2013148. Elsevier, Supplement C, Amsterdam (2003)"},{"key":"1012_CR9","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-662-43652-3_29","volume-title":"International Conference on Abstract State Machines, Alloy, B, VDM, and Z","author":"A Cunha","year":"2014","unstructured":"Cunha, A.: Bounded model checking of temporal formulas with Alloy. In: International Conference on Abstract State Machines, Alloy, B, VDM, and Z, pp. 303\u2013308. Springer, Berlin Heidelberg (2014)"},{"key":"1012_CR10","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: Foundations of Software Engineering, ACM, pp. 373\u2013383 (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"1012_CR11","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/s10270-019-00763-8","volume":"19","author":"S Farheen","year":"2020","unstructured":"Farheen, S., Day, N.A., Vakili, A., Abbassi, A.: Transitive-closure-based model checking (TCMC) in Alloy. J. Softw. Syst. Modell. 19, 721\u2013740 (2020)","journal-title":"J. Softw. Syst. Modell."},{"key":"1012_CR12","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., L\u00f3pez\u00a0Pombo, C.G., Aguirre, N.M.: DynAlloy: Upgrading Alloy with actions. In: International Conference on Software Engineering, ACM, pp. 442\u2013451 (2005a)","DOI":"10.1145\/1062455.1062535"},{"issue":"3","key":"1012_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"1012_CR14","unstructured":"UML (2017) Unified modeling language. https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF, [Online; accessed 28-May-2021]"},{"key":"1012_CR15","doi-asserted-by":"crossref","unstructured":"Serna, J., Day, N.A., Farheen, S.: Dash: A new language for declarative behavioural requirements with control state hierarchy. In: IEEE International Requirements Engineering Conference Workshops (REW), IEEE, pp. 64\u201368 (2017)","DOI":"10.1109\/REW.2017.70"},{"key":"1012_CR16","unstructured":"xtext (2021) Xtext. https:\/\/eclipse.org\/Xtext\/, [Online; accessed 28-May-2021]"},{"key":"1012_CR17","doi-asserted-by":"crossref","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 632\u2013647 (2007)","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"1012_CR18","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grunberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"2","key":"1012_CR19","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. J. 15(2), 235\u2013265 (2010)","journal-title":"Requir. Eng. J."},{"key":"1012_CR20","doi-asserted-by":"crossref","unstructured":"von der Beeck, M.: A comparison of statecharts variants. Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, Lecture Notes In Computer Science 863, 128\u2013148 (1994)","DOI":"10.1007\/3-540-58468-4_163"},{"key":"1012_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0791-0","volume-title":"Formal Specification: Techniques and Applications","author":"N Nissanke","year":"1999","unstructured":"Nissanke, N.: Formal Specification: Techniques and Applications. Springer Verlag, Berlin (1999)"},{"key":"1012_CR22","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. International Series in Computer Science, Prentice Hall (1992)","edition":"2"},{"key":"1012_CR23","doi-asserted-by":"crossref","unstructured":"Elrad, T., Aldawud, O., Bader, A.: Aspect-oriented modeling: Bridging the gap between implementation and design. In: Generative Programming and Component Engineering, Springer, pp. 189\u2013201 (2002)","DOI":"10.1007\/3-540-45821-2_12"},{"issue":"1","key":"1012_CR24","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1016\/S0304-3975(01)00381-4","volume":"290","author":"A Maggiolo-Schettini","year":"2003","unstructured":"Maggiolo-Schettini, A., Peron, A., Tini, S.: A comparison of statecharts step semantics. Theor. Comput. Sci. 290(1), 465\u2013498 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"10","key":"1012_CR25","doi-asserted-by":"publisher","first-page":"866","DOI":"10.1109\/TSE.2003.1237169","volume":"29","author":"J Niu","year":"2003","unstructured":"Niu, J., Atlee, J.M., Day, N.A.: Template semantics for model-based notations. IEEE Trans. Softw. Eng. 29(10), 866\u2013882 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1012_CR26","unstructured":"McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Machine Intelligence 4, Edinburgh University Press, pp. 463\u2013502 (1969)"},{"key":"1012_CR27","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A New Symbolic Model Verifier. In: Proceedings of the 11th International Conference on Computer Aided Verification, pp. 495\u2013499 (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"1012_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: The SMV system. http:\/\/www.kenmcmil.com\/language.ps (1992)","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"1012_CR29","unstructured":"Lu, Y., Atlee, J.M., Day, N.A., Niu, J.: Mapping template semantics to SMV. In: Automated Software Engineering, IEEE Computer Society, pp. 320\u2013325 (2004)"},{"key":"1012_CR30","unstructured":"Cofer, D., Miller, S.P.: Formal methods case studies for DO-333. Tech. Rep. NASA\/CR2014-218244, NASA Langley Research Center (2014)"},{"key":"1012_CR31","unstructured":"Seater, R., Dennis, G.: (n.d.) Tutorial for Alloy Analyzer 4.0. http:\/\/alloytools.org\/tutorials\/online\/index.html, [Online; accessed 28-May-2021]"},{"key":"1012_CR32","unstructured":"Farheen, S.: Improvements to transitive-closure-based model checking in Alloy. MMath thesis, University of Waterloo, David R. Cheriton School of Computer Science (2018)"},{"key":"1012_CR33","unstructured":"Wayne, H.: Formally specifying UIs. https:\/\/hillelwayne.com\/post\/formally-specifying-uis\/, [Online; accessed 28-May-2021] (2018)"},{"key":"1012_CR34","doi-asserted-by":"crossref","unstructured":"Kember, M., Tran, L., Gao, G., Day, N.A.: Extracting counterexamples from transitive-closure-based model checking. In: Modelling in Software Engineering (MISE), a workshop of the International Conference on Software Engineering, ACM, pp. 47\u201354 (2019)","DOI":"10.1109\/MiSE.2019.00015"},{"key":"1012_CR35","doi-asserted-by":"crossref","unstructured":"Mahony, B., Dong. J.S.: Blending object-Z and timed CSP: an introduction to TCOZ. In: International Conference on Software Engineering, IEEE, pp. 95\u2013104 (1998)","DOI":"10.1109\/ICSE.1998.671106"},{"key":"1012_CR36","doi-asserted-by":"crossref","unstructured":"Dong, J.S., Hao, P., Qin, S.C., Sun, J., Yi, W.: Timed patterns: TCOZ to timed automata. In: International Conference on Formal Engineering Methods, Springer, pp. 483\u2013498 (2004)","DOI":"10.1007\/978-3-540-30482-1_39"},{"key":"1012_CR37","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Cavalcanti, A.: A concurrent language for refinement. In: Proceedings of the 5th Irish Conference on Formal Methods, BCS Learning and Development Ltd., pp. 93\u2013115 (2001)","DOI":"10.14236\/ewic\/IWFM2001.7"},{"key":"1012_CR38","doi-asserted-by":"crossref","unstructured":"Mota, A., Farias, A., Didier, A., Woodcock, J.: Rapid prototyping of a semantically well founded circus model checker. In: International Conference on Software Engineering and Formal Methods, Springer, pp. 235\u2013249 (2014)","DOI":"10.1007\/978-3-319-10431-7_17"},{"key":"1012_CR39","doi-asserted-by":"crossref","unstructured":"Gomes, A.O., Butterfield, A.: Circus2csp: A tool for model-checking circus using FDR. In: International Symposium on Formal Methods, Springer, pp. 235\u2013242 (2019)","DOI":"10.1007\/978-3-030-30942-8_15"},{"issue":"1","key":"1012_CR40","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2005.11.007","volume":"354","author":"M Roggenbach","year":"2006","unstructured":"Roggenbach, M.: CSP-CASL-a new integration of process algebra and algebraic specification. Theor. Comput. Sci. 354(1), 42\u201371 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"1012_CR41","doi-asserted-by":"crossref","unstructured":"Reggio, G., Repetto, L.: CASL-CHART: a combination of statecharts and of the algebraic specification language CASL. In: International Conference on Algebraic Methodology and Software Technology, Springer, pp. 243\u2013257 (2000)","DOI":"10.1007\/3-540-45499-3_19"},{"issue":"1\u20132","key":"1012_CR42","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0164-1212(02)00161-9","volume":"70","author":"JP Gruer","year":"2004","unstructured":"Gruer, J.P., Hilaire, V., Koukam, A., Rovarini, P.: Heterogeneous formal specification based on object-Z and statecharts: semantics and verification. J. Syst. Softw. 70(1\u20132), 95\u2013105 (2004)","journal-title":"J. Syst. Softw."},{"key":"1012_CR43","doi-asserted-by":"crossref","unstructured":"Chang, F.S.H., Jackson, D.: Symbolic Model Checking of Declarative Relational Models. In: International Conference on Software Engineering, pp. 312\u2013320 (2006)","DOI":"10.1145\/1134285.1134329"},{"issue":"4","key":"1012_CR44","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1145\/1101815.1101819","volume":"14","author":"MF Frias","year":"2005","unstructured":"Frias, M.F., L\u00f3pez Pombo, C.G., Baum, G.A., Aguirre, N.M., Maibaum, T.S.E.: Reasoning about static and dynamic properties in Alloy. ACM Trans. Softw. Eng. Methodol 14(4), 478\u2013526 (2005)","journal-title":"ACM Trans. Softw. Eng. Methodol"},{"key":"1012_CR45","doi-asserted-by":"crossref","unstructured":"Regis, G., Cornejo, C., Guti\u00e9rrez\u00a0Brida, S., Politano, M., Raverta, F., Ponzio, P., Aguirre, N., Galeotti, J.P., Frias, M.: DynAlloy analyzer: A tool for the specification and analysis of Alloy models with dynamic behaviour. In: Foundations of Software Engineering, ACM, pp. 969\u2013973 (2017)","DOI":"10.1145\/3106237.3122826"},{"key":"1012_CR46","unstructured":"OCL (2014) Object constraint language. http:\/\/www.omg.org\/spec\/OCL\/2.4\/PDF, [Online; accessed 28-May-2021]"},{"key":"1012_CR47","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc, Hoboken (1990)","edition":"2"},{"key":"1012_CR48","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"1012_CR49","volume-title":"Abstract state machines: a method for high-level system design and analysis","author":"E B\u00f6rger","year":"2012","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract state machines: a method for high-level system design and analysis. Springer, Berlin (2012)"},{"key":"1012_CR50","doi-asserted-by":"crossref","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Correct Hardware Design and Verification Methods, pp. 54\u201366 (1999)","DOI":"10.1007\/3-540-48153-2_6"},{"key":"1012_CR51","unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., et\u00a0al.: An overview of SAL. In: Proceedings of the 5th NASA Langley Formal Methods Workshop (2000)"},{"key":"1012_CR52","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Computer-Aided Verification, Springer, pp. 496\u2013500 (2004)","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"1012_CR53","doi-asserted-by":"crossref","unstructured":"Sekerinski, E.: Graphical design of reactive systems. In: International B Conference, Springer, pp. 182\u2013197 (1998)","DOI":"10.1007\/BFb0053361"},{"key":"1012_CR54","unstructured":"Fakhroutdinov, K.: (n.d.) Java 6 thread states and life cycle. https:\/\/www.uml-diagrams.org\/examples\/java-6-thread-state-machine-diagram-example.html, [Online; accessed 28-May-2021]"},{"key":"1012_CR55","unstructured":"Ostroff, J.S.: Validating software via abstract state specifications. Tech. Rep. EECS-2017-02, York University (2017)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01012-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-01012-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01012-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,30]],"date-time":"2024-09-30T21:43:15Z","timestamp":1727732595000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-01012-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,6]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["1012"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-01012-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2022,8,6]]},"assertion":[{"value":"17 June 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 December 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 April 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}