{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T08:53:22Z","timestamp":1762505602089},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,4,14]],"date-time":"2010-04-14T00:00:00Z","timestamp":1271203200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Requirements Eng"],"published-print":{"date-parts":[[2010,6]]},"DOI":"10.1007\/s00766-010-0102-z","type":"journal-article","created":{"date-parts":[[2010,4,13]],"date-time":"2010-04-13T09:02:14Z","timestamp":1271149334000},"page":"235-265","source":"Crossref","is-referenced-by-count":20,"title":["Deconstructing the semantics of big-step modelling languages"],"prefix":"10.1007","volume":"15","author":[{"given":"Shahram","family":"Esmaeilsabzali","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joanne M.","family":"Atlee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwei","family":"Niu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,4,14]]},"reference":[{"key":"102_CR1","unstructured":"The Esterel v7 reference manual version v7.30, initial IEEE standardization proposal (2005)"},{"issue":"7","key":"102_CR2","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1109\/TSE.2003.1214326","volume":"29","author":"R Alur","year":"2003","unstructured":"Alur R, Etessami K, Yannakakis M (2003) Inference of message sequence charts. IEEE Trans Softw Eng 29(7):623\u2013633","journal-title":"IEEE Trans Softw Eng"},{"issue":"1","key":"102_CR3","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger TA (1999) Reactive modules. Form Method Syst Des 15(1):7\u201348","journal-title":"Form Method Syst Des"},{"issue":"1","key":"102_CR4","first-page":"95","volume":"17","author":"G Berry","year":"1992","unstructured":"Berry G (1992) A hardware implementation of pure Esterel. Sadhana Acad Proc Eng Sci Indian Acad Sci 17(1):95\u2013130","journal-title":"Sadhana Acad Proc Eng Sci Indian Acad Sci"},{"key":"102_CR5","doi-asserted-by":"crossref","unstructured":"Berry G (1993) Preemption in concurrent systems. In: Foundations of software technology and theoretical computer science, vol 761 of LNCS. Springer, pp 72\u201393","DOI":"10.1007\/3-540-57529-4_44"},{"issue":"2","key":"102_CR6","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry G, Gonthier G (1992) The Esterel synchronous programming language: design, semantics, implementation. Sci Comp Programm 19(2):87\u2013152","journal-title":"Sci Comp Programm"},{"key":"102_CR7","unstructured":"Boussinot F (1998) Sugarcubes implementation of causality. Technical Report RR-3487, Inria, Institut National de Recherche en Informatique et en Automatique"},{"key":"102_CR8","unstructured":"Chapiro DM (1984) Globally-asynchronous locally-synchronous systems. PhD thesis, Stanford University"},{"key":"102_CR9","volume-title":"Mastering simulink","author":"J Dabney","year":"2004","unstructured":"Dabney J, Harman TL (2004) Mastering simulink. Pearson Prentice Hall, New Jersey"},{"key":"102_CR10","unstructured":"Day N (1993) A model checker for statecharts: linking CASE tools with formal methods. Master\u2019s thesis, University of British Columbia"},{"key":"102_CR11","doi-asserted-by":"crossref","unstructured":"de Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of the joint 8th European software engineering conference and 9th ACM SIGSOFT symposium on the foundation of software engineering (ESEC\/FSE-01), Software engineering notes, vol 26. ACM Press, pp 109\u2013120","DOI":"10.1145\/503209.503226"},{"key":"102_CR12","doi-asserted-by":"crossref","unstructured":"Esmaeilsabzali S, Day NA (2010) Prescriptive semantics for big-step modelling languages. In: Fundamental approaches to software engineering, volume 6013 of LNCS. Springer, pp 158\u2013172","DOI":"10.1007\/978-3-642-12029-9_12"},{"key":"102_CR13","unstructured":"Esmaeilsabzali S, Day NA, Atlee JM, Niu J (2009) Big-step semantics. Technical Report CS-2009-05, University of Waterloo, Cheriton School of Computer Science"},{"key":"102_CR14","doi-asserted-by":"crossref","unstructured":"Esmaeilsabzali S, Day NA, Atlee JM, Niu J (2009) Semantic criteria for choosing a language for big-step models. In: 17th IEEE international requirements engineering conference. IEEE Computer Society Press, pp 181\u2013190","DOI":"10.1109\/RE.2009.29"},{"key":"102_CR15","unstructured":"Fidge C (1994) A comparative introduction to CSP, CCS and LOTOS. Technical Report 93-24, The university of Queensland, Department of Computer Science"},{"key":"102_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous programming of reactive systems","author":"N Halbwachs","year":"1993","unstructured":"Halbwachs Nicolas (1993) Synchronous programming of reactive systems. Kluwer, Dordrecht"},{"issue":"3","key":"102_CR17","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comp Programm 8(3):231\u2013274","journal-title":"Sci Comp Programm"},{"key":"102_CR18","doi-asserted-by":"crossref","unstructured":"Harel D, Kugler H (2004) The RHAPSODY semantics of statecharts (or, on the executable core of the UML). In: Integration of software specification techniques for application in engineering, volume 3147 of LNCS. Springer, pp 325\u2013354","DOI":"10.1007\/978-3-540-27863-4_19"},{"issue":"4","key":"102_CR19","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel D, Naamad A (1996) The STATEMATE semantics of statecharts. ACM Trans Softw Eng Methodol 5(4):293\u2013333","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"102_CR20","doi-asserted-by":"crossref","unstructured":"Harel D, Pnueli A (1985) On the development of reactive systems. In: Logics and models of concurrent systems. Springer","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"102_CR21","unstructured":"Harel D, Pnueli A, Schmidt JP, Sherman R (1987) On the formal semantics of statecharts. In: IEEE symposium on logic in computation. pp 54\u201364"},{"issue":"3","key":"102_CR22","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"CL Heitmeyer","year":"1996","unstructured":"Heitmeyer CL, Jeffords RD, Labaw BG (1996) Automated consistency checking of requirements specifications. ACM Trans Softw Eng Methodol 5(3):231\u2013261","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"102_CR23","unstructured":"Heninger KL, Kallander JW, Parnas DL, Shore JE (1978) Software requirements for the A-7E aircraft. Technical Report 3876, United States Naval Research Laboratory"},{"key":"102_CR24","volume-title":"Communicating sequential processes","author":"T Hoare","year":"1985","unstructured":"Hoare T (1985) Communicating sequential processes. Prentice Hall, New Jersey"},{"key":"102_CR25","volume-title":"Unifying theories of programming","author":"T Hoare","year":"1998","unstructured":"Hoare T, Jifeng H (1998) Unifying theories of programming. Prentice Hall, New Jersey"},{"key":"102_CR26","doi-asserted-by":"crossref","unstructured":"Huizing C, Gerth R (1992) Semantics of reactive systems in abstract time. In: REX Workshop, volume 600 of LNCS. Springer, pp 291\u2013314","DOI":"10.1007\/BFb0031997"},{"key":"102_CR27","unstructured":"i Logix Inc (1991) Statemate 4.0 analyzer user and reference manual"},{"key":"102_CR28","doi-asserted-by":"crossref","unstructured":"Kang KC, Cohen SG, Hess JA, Novak WE, Peterson AS (1990) Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU\/SEI-90-TR-21, SEI, Carnegie Mellon University","DOI":"10.21236\/ADA235785"},{"key":"102_CR29","unstructured":"Lamport L, Schneider FB (1989) Pretending atomicity. Technical Report 44, Digital Equipment Corporation"},{"issue":"9","key":"102_CR30","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"NG Leveson","year":"1994","unstructured":"Leveson NG, Heimdahl MPE, Hildreth H, Reese JD (1994) Requirements specification for process-control systems. IEEE Trans Softw Eng 20(9):684\u2013707","journal-title":"IEEE Trans Softw Eng"},{"key":"102_CR31","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton RJ (1975) Reduction: a method of proving properties of parallel programs. Commun ACM 18:717\u2013721","journal-title":"Commun ACM"},{"key":"102_CR32","doi-asserted-by":"crossref","unstructured":"Maggiolo-Schettini A, Peron A, Tini S (1996) Equivalences of statecharts. In: International concurrency theory conference, volume 1119 of LNCS. Springer, pp 687\u2013702","DOI":"10.1007\/3-540-61604-7_84"},{"issue":"1\/3","key":"102_CR33","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/S0096-0551(01)00016-9","volume":"27","author":"F Maraninchi","year":"2001","unstructured":"Maraninchi F, R\u00e9mond Y (2001) Argos: an automaton-based synchronous language. Comp Lang 27(1\/3):61\u201392","journal-title":"Comp Lang"},{"key":"102_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking: an approach to the state explosion problem","author":"K McMillan","year":"1993","unstructured":"McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer, Dordrecht"},{"key":"102_CR35","doi-asserted-by":"crossref","unstructured":"Milner R (1983) Calculi for synchrony and asynchrony. Theor Comp Sci 25(3):267\u2013310 (Fundamental study)","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"102_CR36","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall, New Jersey"},{"issue":"10","key":"102_CR37","doi-asserted-by":"crossref","first-page":"866","DOI":"10.1109\/TSE.2003.1237169","volume":"29","author":"J Niu","year":"2003","unstructured":"Niu J, Atlee JM, Day NA (2003) Template semantics for model-based notations. IEEE Trans Softw Eng 29(10):866\u2013882","journal-title":"IEEE Trans Softw Eng"},{"key":"102_CR38","unstructured":"OMG (2007) OMG unified modeling language (OMG UML), superstructure, v2.1.2. Formal\/2007-11-01"},{"issue":"1","key":"102_CR39","first-page":"19","volume":"25","author":"DL Parnas","year":"1995","unstructured":"Parnas DL, Madey J (1995) Functional documents for computer systems. Sci Comp Programm 25(1):19\u201323","journal-title":"Sci Comp Programm"},{"key":"102_CR40","volume-title":"Types and programming languages","author":"BC Pierce","year":"2002","unstructured":"Pierce BC (2002) Types and programming languages. MIT Press, Cambridge"},{"key":"102_CR41","first-page":"373","volume-title":"Liber Amicorum","author":"A Pnueli","year":"1989","unstructured":"Pnueli A, Shalev M (1989) What is in a step? In: De Bakker JW (ed) Liber Amicorum. CWI, Amsterdam, pp 373\u2013400"},{"key":"102_CR42","doi-asserted-by":"crossref","unstructured":"Pnueli A, Shalev M (1991) What is in a step: on the semantics of statecharts. In: Theoretical aspects of computer Software, volume 526 of LNCS. Springer, pp 244\u2013264","DOI":"10.1007\/3-540-54415-1_49"},{"issue":"1\u20132","key":"102_CR43","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/S0304-3975(96)80710-9","volume":"170","author":"V Sassone","year":"1996","unstructured":"Sassone V, Nielsen M, Winskel G (1996) Models for concurrency: towards a classification. Theor Comp Sci 170(1\u20132):297\u2013348","journal-title":"Theor Comp Sci"},{"issue":"2","key":"102_CR44","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s10703-006-7840-z","volume":"28","author":"SK Shukla","year":"2006","unstructured":"Shukla SK, Theobald M (2006) Special issue on formal methods for globally asynchronous and locally synchronous (GALS) systems. Formal Methods Syst Des 28(2):91\u201392","journal-title":"Formal Methods Syst Des"},{"issue":"3","key":"102_CR45","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1023\/A:1022902408130","volume":"22","author":"SJ Silver","year":"2003","unstructured":"Silver SJ, Brzozowski JA (2003) True concurrency in models of asynchronous circuit behavior. Formal Methods Syst Des 22(3):183\u2013203","journal-title":"Formal Methods Syst Des"},{"key":"102_CR46","doi-asserted-by":"crossref","unstructured":"Taleghani A, Atlee JM (2006) Semantic variations among UML StateMachines. In: Model driven engineering languages and systems, 9th international conference, volume 4199 of LNCS. Springer, pp 245\u2013259","DOI":"10.1007\/11880240_18"},{"issue":"2","key":"102_CR47","doi-asserted-by":"crossref","first-page":"8:1","DOI":"10.1145\/1216374.1216376","volume":"29","author":"O Tardieu","year":"2007","unstructured":"Tardieu O (2007) A deterministic logical semantics for pure Esterel. ACM Trans Programm Lang Syst 29(2):8:1\u20138:26","journal-title":"ACM Trans Programm Lang Syst"},{"key":"102_CR48","unstructured":"van Glabbeek R. The linear time\u2014branching time spectrum. In: International concurrency theory conference, volume 458 of LNCS"},{"key":"102_CR49","doi-asserted-by":"crossref","unstructured":"von der Beeck M (1994) A comparison of statecharts variants. In: Formal techniques in real-time and fault-tolerant systems, volume 863 of LNCS. Springer, pp 128\u2013148","DOI":"10.1007\/3-540-58468-4_163"},{"issue":"1","key":"102_CR50","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/237432.237434","volume":"6","author":"P Zave","year":"1997","unstructured":"Zave P, Jackson M (1997) Four dark corners of requirements engineering. ACM Trans Softw Eng Methodol 6(1):1\u201330","journal-title":"ACM Trans Softw Eng Methodol"}],"container-title":["Requirements Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-010-0102-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00766-010-0102-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-010-0102-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T05:59:28Z","timestamp":1559109568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00766-010-0102-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,14]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["102"],"URL":"https:\/\/doi.org\/10.1007\/s00766-010-0102-z","relation":{},"ISSN":["0947-3602","1432-010X"],"issn-type":[{"value":"0947-3602","type":"print"},{"value":"1432-010X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,14]]}}}