{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T08:18:55Z","timestamp":1709367535686},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,1,3]],"date-time":"2020-01-03T00:00:00Z","timestamp":1578009600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,3]],"date-time":"2020-01-03T00:00:00Z","timestamp":1578009600000},"content-version":"vor","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":[[2020,5]]},"DOI":"10.1007\/s10270-019-00763-8","type":"journal-article","created":{"date-parts":[[2020,1,3]],"date-time":"2020-01-03T09:03:16Z","timestamp":1578042196000},"page":"721-740","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Transitive-closure-based model checking (TCMC) in Alloy"],"prefix":"10.1007","volume":"19","author":[{"given":"Sabria","family":"Farheen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amirhossein","family":"Vakili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Abbassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,1,3]]},"reference":[{"key":"763_CR1","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":"763_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Chechik, M. (ed.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"763_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E.: The ASM method for system design and analysis. A tutorial introduction. In: Frontiers of Combining Systems, Lecture Notes in Computer Science, vol. 3717, pp. 264\u2013283. Springer (2005)","DOI":"10.1007\/11559306_15"},{"key":"763_CR4","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: International Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 6538, pp. 70\u201387. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"763_CR5","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. ACM (2006)","DOI":"10.1145\/1134285.1134329"},{"key":"763_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Computer Aided Verification, Lecture Notes In Computer Science, vol. 2404, pp. 241\u2013268. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"763_CR7","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Boca Raton (1999)"},{"key":"763_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Form. Methods Syst. Design 10, 47\u201371 (1997)","journal-title":"Form. Methods Syst. Design"},{"key":"763_CR9","doi-asserted-by":"crossref","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 (2014)","DOI":"10.1007\/978-3-662-43652-3_29"},{"key":"763_CR10","doi-asserted-by":"crossref","unstructured":"Del Castillo, G., Winter, K.: Model checking support for the ASM high-level language. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes In Computer Science, vol. 1785, pp. 331\u2013346. Springer (2000)","DOI":"10.1007\/3-540-46419-0_23"},{"issue":"8","key":"763_CR11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"763_CR12","unstructured":"Dold, A.: A formal representation of abstract state machines using PVS. Verifix Technical Report Ulm\/6.2, Universit\u00e4t Ulm (1998)"},{"key":"763_CR13","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol. 2919, pp. 333\u2013336. Springer (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"763_CR14","unstructured":"Farheen, S.: Improvements to transitive-closure-based model checking in Alloy. M.Math thesis, University of Waterloo, David R. Cheriton School of Computer Science (2018)"},{"key":"763_CR15","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., L\u00f3pez Pombo, C.G., Aguirre, N.M.: DynAlloy: upgrading Alloy with actions. In: International Conference on Software Engineering, pp. 442\u2013451. ACM (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"763_CR16","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. In: Proccedings of 2nd International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 527, pp. 250\u2013265. Springer (1991)","DOI":"10.1007\/3-540-54430-5_93"},{"key":"763_CR17","doi-asserted-by":"crossref","unstructured":"Immerman, N., Vardi, M.: Model checking and transitive-closure logic. In: Computer-Aided Verification, Lecture Notes in Computer Science, vol. 1254, pp. 291\u2013302. Springer (1997)","DOI":"10.1007\/3-540-63166-6_29"},{"key":"763_CR18","unstructured":"International Organisation for Standardization. Information Technology Z Formal Specification Notation Syntax, Type System and Semantics (2000)"},{"issue":"2","key":"763_CR19","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"763_CR20","volume-title":"Software Abstractions\u2014Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions\u2014Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"763_CR21","doi-asserted-by":"crossref","unstructured":"Kember, M., Tran, L., Gao, G., Day, N.A.: Extracting counterexamples from transitive-closure-based model checking. In: Workshop on Modelling in Software Engineering (MISE)@ International Conference on Software Engineering (ICSE), pp. 47\u201354. ACM (2019)","DOI":"10.1109\/MiSE.2019.00015"},{"key":"763_CR22","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2017.08.013","volume":"15","author":"S Krings","year":"2018","unstructured":"Krings, S., Leuschel, M.: Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci. Comput. Program. 15, 41\u201363 (2018)","journal-title":"Sci. Comput. Program."},{"key":"763_CR23","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10, 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"763_CR24","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, pp. 373\u2013383. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"763_CR25","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic model checking: an approach to the state explosion problem. Ph.D. thesis, Pittsburgh, PA, USA (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"763_CR26","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering, vol. 1, 609\u2013619. IEEE (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"763_CR27","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, 1st edn. Springer, Berlin (1999)","edition":"1"},{"issue":"1","key":"763_CR28","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0167-6423(00)00018-6","volume":"41","author":"M Plath","year":"2001","unstructured":"Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53\u201384 (2001)","journal-title":"Sci. Comput. Program."},{"key":"763_CR29","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, pp. 969\u2013973. ACM (2017)","DOI":"10.1145\/3106237.3122826"},{"issue":"4","key":"763_CR30","first-page":"377","volume":"3","author":"G Schellhorn","year":"1997","unstructured":"Schellhorn, G., Ahrendt, W.: Reasoning about abstract state machines: the WAM case study. J. Univers. Comput. Sci. 3(4), 377\u2013413 (1997)","journal-title":"J. Univers. Comput. Sci."},{"key":"763_CR31","doi-asserted-by":"crossref","unstructured":"Selic, B.: From model-driven development to model-driven engineering. In: Euromicro Conference on Real-Time Systems. IEEE Computer Society (2007)","DOI":"10.1109\/ECRTS.2007.16"},{"key":"763_CR32","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: International workshop on model-driven requirements engineering (MoDRE)@ IEEE international requirements engineering conference (RE), pp. 64\u201368 (2017)","DOI":"10.1109\/REW.2017.70"},{"key":"763_CR33","unstructured":"Vakili, A.: Temporal logic model checking as automated theorem proving. Ph.D. thesis, University of Waterloo, David R. Cheriton School of Computer Science (2016)"},{"key":"763_CR34","doi-asserted-by":"crossref","unstructured":"Vakili, A., Day, N.A.: Temporal model checking in alloy. In: International Conference on Abstract State Machines, Alloy, B, VDM, and Z, Lecture Notes In Computer Science, vol. 7316, pp. 150\u2013163. Springer (2012)","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"763_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115, 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"763_CR36","doi-asserted-by":"crossref","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 54\u201366. Springer (1999)","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-019-00763-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-019-00763-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-019-00763-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,2]],"date-time":"2021-01-02T00:36:48Z","timestamp":1609547808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-019-00763-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,3]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,5]]}},"alternative-id":["763"],"URL":"https:\/\/doi.org\/10.1007\/s10270-019-00763-8","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,1,3]]},"assertion":[{"value":"1 October 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2019","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 October 2019","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 January 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}