{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T22:02:20Z","timestamp":1767996140101,"version":"3.49.0"},"reference-count":67,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100009567","name":"Budapest University of Technology and Economics","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100009567","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2020,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.\n<\/jats:p>","DOI":"10.1007\/s10270-020-00806-5","type":"journal-article","created":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T06:32:31Z","timestamp":1593585151000},"page":"1483-1517","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Mixed-semantics composition of statecharts for the component-based design of reactive systems"],"prefix":"10.1007","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5546-5970","authenticated-orcid":false,"given":"Bence","family":"Graics","sequence":"first","affiliation":[]},{"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[]},{"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[]},{"given":"D\u00e1niel","family":"Varr\u00f3","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,1]]},"reference":[{"issue":"11","key":"806_CR1","doi-asserted-by":"publisher","first-page":"2104","DOI":"10.1109\/JPROC.2015.2453253","volume":"103","author":"P Nuzzo","year":"2015","unstructured":"Nuzzo, P., Sangiovanni-Vincentelli, A.L., Bresolin, D., Geretti, L., Villa, T.: A platform-based design methodology with contracts and related tools for the design of cyber-physical systems. Proc. IEEE 103(11), 2104\u20132132 (2015)","journal-title":"Proc. IEEE"},{"key":"806_CR2","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, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"806_CR3","doi-asserted-by":"crossref","unstructured":"Latella, D., Majzik, I., Massink, M.: Towards a formal operational semantics of UML statechart diagrams. In: Formal Methods for Open Object-Based Distributed Systems, Springer, pp.\u00a0331\u2013347 (1999)","DOI":"10.1007\/978-0-387-35562-7_25"},{"key":"806_CR4","unstructured":"Crane, M.\u00a0L., Dingel, J.: On the semantics of UML state machines: categorization and comparision. In: In Technical Report 2005-501, School of Computing, Queen\u2019s (2005)"},{"key":"806_CR5","unstructured":"Group, O.\u00a0M.: Semantics of a foundational subset for executable UML models. Technical Report formal\/2018-12-01, Object Management Group (2018)"},{"key":"806_CR6","unstructured":"Group, O.\u00a0M.: Precise semantics of UML state machines (PSSM). Technical Report formal\/2019-05-01, Object Management Group (2019)"},{"key":"806_CR7","unstructured":"Group, O.\u00a0M.: Precise semantics of UML composite structures (PSCS). Technical Report formal\/2019-02-01, Object Management Group (2019)"},{"key":"806_CR8","doi-asserted-by":"crossref","unstructured":"Crane, M.\u00a0L., Dingel, J.: UML versus classical versus Rhapsody statecharts: not all models are created equal. In: Briand, L., Williams, C. (eds.), Model Driven Engineering Languages and Systems, Springer, Heidelberg, pp.\u00a097\u2013112 (2005)","DOI":"10.1007\/11557432_8"},{"issue":"3","key":"806_CR9","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.scico.2008.09.001","volume":"74","author":"R Eshuis","year":"2009","unstructured":"Eshuis, R.: Reconciling statechart semantics. Sci. Comput Program. 74(3), 65\u201399 (2009)","journal-title":"Sci. Comput Program."},{"key":"806_CR10","doi-asserted-by":"crossref","unstructured":"Moln\u00e1r, V., Graics, B., V\u00f6r\u00f6s, A., Majzik, I., Varr\u00f3, D.: The Gamma Statechart Composition Framework. In: 40th International Conference on Software Engineering (ICSE 2018), ACM, Gothenburg, Sweden (2018)","DOI":"10.1145\/3183440.3183489"},{"key":"806_CR11","unstructured":"Behrmann, G., David, A., Larsen, K.\u00a0G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0 (2006)"},{"key":"806_CR12","doi-asserted-by":"crossref","unstructured":"V\u00f6r\u00f6s, A., B\u00far, M., R\u00e1th, I., Horv\u00e1th, \u00c1., Micskei, Z., Balogh, L., Hegyi, B., Horv\u00e1th, B., M\u00e1zl\u00f3, Z., Varr\u00f3, D.: MoDeS3: model-based demonstrator for smart and safe cyber-physical systems. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.), NASA Formal Methods, Springer, Cham, pp.\u00a0460\u2013467 (2018)","DOI":"10.1007\/978-3-319-77935-5_31"},{"key":"806_CR13","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/5.381846","volume":"83","author":"EA Lee","year":"1995","unstructured":"Lee, E.A., Parks, T.M.: Dataflow process networks. Proc. IEEE 83, 773\u2013801 (1995)","journal-title":"Proc. IEEE"},{"issue":"9","key":"806_CR14","doi-asserted-by":"publisher","first-page":"1270","DOI":"10.1109\/5.97297","volume":"79","author":"A Benveniste","year":"1991","unstructured":"Benveniste, A., Berry, G.: The synchronous approach to reactive and real-time systems. Proc. IEEE 79(9), 1270\u20131282 (1991)","journal-title":"Proc. IEEE"},{"issue":"9","key":"806_CR15","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"issue":"1","key":"806_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0167-6423(02)00096-5","volume":"48","author":"SA Edwards","year":"2003","unstructured":"Edwards, S.A., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Sci. Comput. Program. 48(1), 21\u201342 (2003)","journal-title":"Sci. Comput. Program."},{"key":"806_CR17","volume-title":"Model Checking","author":"EM Clarke Jr","year":"2018","unstructured":"Clarke Jr., E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. MIT press, Cambridge (2018)"},{"key":"806_CR18","doi-asserted-by":"crossref","unstructured":"Dwyer, M.\u00a0B., Avrunin, G.\u00a0S., Corbett, J.\u00a0C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), pp.\u00a0411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"806_CR19","first-page":"145","volume":"2010","author":"\u00c1 Heged\u00fcs","year":"2010","unstructured":"Heged\u00fcs, \u00c1., Bergmann, G., R\u00e1th, I., Varr\u00f3, D.: Back-annotation of simulation traces with change-driven model transformations. Proc. Softw. Eng. Formal Methods (SEFM) 2010, 145\u2013155 (2010)","journal-title":"Proc. Softw. Eng. Formal Methods (SEFM)"},{"key":"806_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1002\/stvr.456","volume":"22","author":"M Utting","year":"2012","unstructured":"Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22, 297\u2013312 (2012)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"806_CR21","doi-asserted-by":"crossref","unstructured":"Liu, S., Liu, Y., Andr\u00e9, \u00c9., Choppy, C., Sun, J., Wadhwa, B., Dong, J.\u00a0S.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.), Integrated Formal Methods, Springer, Berlin, pp.\u00a0331\u2013346 (2013)","DOI":"10.1007\/978-3-642-38613-8_23"},{"key":"806_CR22","first-page":"87","volume-title":"Timed Automata: Semantics, Algorithms and Tools","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools, pp. 87\u2013124. Springer, Berlin (2004)"},{"key":"806_CR23","unstructured":"Wagner, F.: VFSM executable specification. In: CompEuro 1992 Proceedings Computer Systems and Software Engineering, pp.\u00a0226\u2013231 (1992)"},{"key":"806_CR24","unstructured":"Graics, B., Moln\u00e1r, V.: Documentation of the Gamma Statechart Composition Framework v0.9. Technical Report, Budapest University of Technology and Economics, Department of Measurement and Information Systems. https:\/\/inf.mit.bme.hu\/en\/gamma\/ (2016)"},{"issue":"3","key":"806_CR25","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G Fraser","year":"2007","unstructured":"Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215\u2013261 (2007)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"806_CR26","unstructured":"Callahan, J., Schneider, F., Easterbrook, S.: Automated software testing using model-checking (2000)"},{"key":"806_CR27","unstructured":"Graics, B., Majzik, I.: Modeling and analysis of an industrial communication protocol in the Gamma framework. In: 27th Minisymposium, Department of Measurement and Information Systems, Budapest, Hungary (2020)"},{"key":"806_CR28","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/3379106.3379113","volume":"39","author":"S Procter","year":"2020","unstructured":"Procter, S., Feiler, P.: The AADL error library: an operationalized taxonomy of system errors. Ada Lett. 39, 63\u201370 (2020)","journal-title":"Ada Lett."},{"key":"806_CR29","doi-asserted-by":"crossref","unstructured":"Clarke, E.\u00a0M., Emerson, E.\u00a0A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logic of Programs, Springer, pp.\u00a052\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"806_CR30","doi-asserted-by":"crossref","unstructured":"Lohstroh, M., Schoeberl, M., Jan, M., Wang, E., Lee, E.\u00a0A.: Programs with ironclad timing guarantees: work-in-progress. In: Proceedings of the International Conference on Embedded Software Companion, ACM, New York, NY, USA, October 13\u201318, 2019, p.\u00a01 (2019)","DOI":"10.1145\/3349568.3351553"},{"key":"806_CR31","doi-asserted-by":"crossref","unstructured":"Sztipanovits, J., Bapty, T., Neema, S., Howard, L., Jackson, E.: OpenMETA: A Model- and Component-Based Design Tool Chain for Cyber-Physical Systems, Springer, Berlin, pp.\u00a0235\u2013248 (2014)","DOI":"10.1007\/978-3-642-54848-2_16"},{"key":"806_CR32","doi-asserted-by":"crossref","unstructured":"Simko, G., Lindecker, D., Levendovszky, T., Neema, S., Sztipanovits, J.: Specification of cyber-physical components with formal semantics\u2014integration and composition. In: Moreira, A., Sch\u00e4tz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.), Model-Driven Engineering Languages and Systems, Springer, Berlin, pp.\u00a0471\u2013487 (2013)","DOI":"10.1007\/978-3-642-41533-3_29"},{"issue":"5","key":"806_CR33","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: Robochart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019)","journal-title":"Softw. Syst. Model."},{"key":"806_CR34","first-page":"12:1","volume":"3","author":"Y Jiang","year":"2018","unstructured":"Jiang, Y., Song, H., Yang, Y., Liu, H., Gu, M., Guan, Y., Sun, J., Sha, L.: Dependable model-driven development of CPS: from stateflow simulation to verified implementation. ACM Trans. Cyber. Phys. Syst. 3, 12:1\u201312:31 (2018)","journal-title":"ACM Trans. Cyber. Phys. Syst."},{"issue":"1","key":"806_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.22152\/programming-journal.org\/2019\/3\/2","volume":"3","author":"P Juodisius","year":"2018","unstructured":"Juodisius, P., Sarkar, A., Mukkamala, R.R., Antkiewicz, M., Czarnecki, K., Wasowski, A.: Clafer: lightweight modeling of structure, behaviour, and variability. Art Sci. Eng. Program. 3(1), 1\u20132 (2018)","journal-title":"Art Sci. Eng. Program."},{"key":"806_CR36","doi-asserted-by":"crossref","unstructured":"Lugou, F., Li, L.\u00a0W., Apvrille, L., Ameur-Boulifa, R.: SysML models and model transformation for security. In: Conference on Model-Driven Engineering and Software Development (Modelsward\u20192016), Rome, Italy (2016)","DOI":"10.5220\/0005748703310338"},{"key":"806_CR37","doi-asserted-by":"crossref","unstructured":"Apvrille, L., Roudier, Y.: Model-Driven Engineering and Software Development, ch.\u00a0Designing Safe and Secure Embedded and Cyber-Physical Systems with SysML-Sec, Springer International Publishing, Dordrecht, pp.\u00a0293\u2013308 (2016)","DOI":"10.1007\/978-3-319-27869-8_17"},{"key":"806_CR38","unstructured":"Haber, A., Ringert, J.\u00a0O., Rumpe, B.: Montiarc architectural modeling of interactive distributed and cyber-physical systems. arXiv:1409.6578 (2014)"},{"issue":"2","key":"806_CR39","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MC.2006.51","volume":"39","author":"A Childs","year":"2006","unstructured":"Childs, A., Greenwald, J., Jung, G., Hoosier, M., Hatcliff, J.: Calm and Cadena: metamodeling for component-based product-line development. Computer 39(2), 42\u201350 (2006)","journal-title":"Computer"},{"key":"806_CR40","doi-asserted-by":"crossref","unstructured":"Feiler, P.\u00a0H., Gluch, D.\u00a0P., Hudak, J.\u00a0J.: The Architecture Analysis and Design Language (AADL): an introduction. Technical Report, Carnegie-Mellon Univ Pittsburgh PA Software Engineering Inst (2006)","DOI":"10.21236\/ADA455842"},{"key":"806_CR41","unstructured":"Reisig, W.: Associative composition of reactive systems. Technical Report, Humboldt-Universit\u00e4t zu Berlin, Institut f\u00fcr Informatik (2017)"},{"key":"806_CR42","doi-asserted-by":"publisher","first-page":"850","DOI":"10.1145\/268999.269004","volume":"44","author":"M Broy","year":"1997","unstructured":"Broy, M.: Compositional refinement of interactive systems. J. ACM 44, 850\u2013891 (1997)","journal-title":"J. ACM"},{"key":"806_CR43","volume-title":"Model Driven Engineering for Distributed Real-Time Embedded Systems","author":"S Gerard","year":"2010","unstructured":"Gerard, S., Babau, J.-P., Champeau, J.: Model Driven Engineering for Distributed Real-Time Embedded Systems. Wiley-IEEE Press, New York (2010)"},{"key":"806_CR44","unstructured":"Chhokra, A., Abdelwahed, S., Dubey, A., Neema, S., Karsai, G.: From system modeling to formal verification. In: The 2015 Electronic System Level Synthesis Conference (2015)"},{"key":"806_CR45","doi-asserted-by":"crossref","unstructured":"Panda, P.\u00a0R.: SystemC: a modeling platform supporting multiple design abstractions. In: Proceedings of the 14th International Symposium on Systems Synthesis, ACM, pp.\u00a075\u201380 (2001)","DOI":"10.1145\/500001.500018"},{"key":"806_CR46","doi-asserted-by":"crossref","unstructured":"Herber, P.: A Framework for Automated HW\/SW Co-Verification of SystemC Designs using Timed Automata, GmbH, Berlin (2010)","DOI":"10.1109\/ETSYM.2010.5512761"},{"key":"806_CR47","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Donatiello, L., Ciancarini, P.: Stochastic process algebra: from an algebraic formalism to an architectural description language. In: IFIP International Symposium on Computer Performance Modeling, Measurement and Evaluation, Springer, pp.\u00a0236\u2013260 (2002)","DOI":"10.1007\/3-540-45798-4_11"},{"key":"806_CR48","unstructured":"Mazzini, S., Favaro, J.\u00a0M., Puri, S., Baracchi, L.: Chess: an open source methodology and toolset for the development of critical systems. In: EduSymp\/OSS4MDE@MoDELS (2016)"},{"key":"806_CR49","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM) 2006, IEEE, pp.\u00a03\u201312 (2006)"},{"issue":"1","key":"806_CR50","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","volume":"91","author":"J Eker","year":"2003","unstructured":"Eker, J., Janneck, J.W., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Sachs, S., Xiong, Y., Neuendorffer, S.: Taming heterogeneity: the Ptolemy approach. Proc. IEEE 91(1), 127\u2013144 (2003)","journal-title":"Proc. IEEE"},{"issue":"12","key":"806_CR51","doi-asserted-by":"publisher","first-page":"1235","DOI":"10.1016\/j.scico.2010.10.002","volume":"77","author":"K Bae","year":"2012","unstructured":"Bae, K., lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using real-time maude. Sci. Comput. Program. 77(12), 1235\u20131271 (2012)","journal-title":"Sci. Comput. Program."},{"key":"806_CR52","doi-asserted-by":"crossref","unstructured":"Selic, B.: Using UML for modeling complex real-time systems. In: Mueller, F., Bestavros, A. (eds.), Languages, Compilers, and Tools for Embedded Systems, Springer, Berlin, pp.\u00a0250\u2013260 (1998)","DOI":"10.1007\/BFb0057795"},{"key":"806_CR53","volume-title":"Real-Time Object-Oriented Modeling","author":"B Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. Wiley, New York (1994)"},{"key":"806_CR54","doi-asserted-by":"crossref","unstructured":"Hili, N., Dingel, J., Beaulieu, A.: Modelling and code generation for real-time embedded systems with UML-RT and Papyrus-RT. In: 2017 IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C), pp.\u00a0509\u2013510 (2017)","DOI":"10.1109\/ICSE-C.2017.168"},{"key":"806_CR55","unstructured":"Zurowska, K.: Language specific analysis of state machine models of reactive systems. Ph. D. Thesis, Queen\u2019s Univerity, Canada (2014)"},{"issue":"2","key":"806_CR56","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s10270-015-0484-y","volume":"16","author":"K Zurowska","year":"2017","unstructured":"Zurowska, K., Dingel, J.: Language-specific model checking of UML-RT models. Softw. Syst. Model. 16(2), 393\u2013415 (2017)","journal-title":"Softw. Syst. Model."},{"key":"806_CR57","doi-asserted-by":"crossref","unstructured":"Rapos, E.\u00a0J., Dingel, J.: Incremental test case generation for UML-RT models using symbolic execution. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp.\u00a0962\u2013963 (2012)","DOI":"10.1109\/ICST.2012.205"},{"key":"806_CR58","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: ACES-MB and WUCOR@ MoDELS, vol.\u00a01508, pp.\u00a019\u201326 (2015)"},{"key":"806_CR59","volume-title":"Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement","author":"M Broy","year":"2012","unstructured":"Broy, M., St\u00f8len, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, Berlin (2012)"},{"key":"806_CR60","unstructured":"Kanav, S., Aravantinos, V.: Modular transformation from AF3 to nuXmv. In: MODELS (Satellite Events), pp.\u00a0300\u2013306 (2017)"},{"key":"806_CR61","volume-title":"Object-Oriented Systems Analysis: Modeling the World in Data","author":"S Shlaer","year":"1988","unstructured":"Shlaer, S., Mellor, S.J.: Object-Oriented Systems Analysis: Modeling the World in Data. Yourdon Press, New York (1988)"},{"key":"806_CR62","doi-asserted-by":"crossref","unstructured":"Ke, X., Sierszecki, K., Angelov, C.: COMDES-II: a component-based framework for generative development of distributed real-time control systems. In: 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2007), pp.\u00a0199\u2013208 (2007)","DOI":"10.1109\/RTCSA.2007.29"},{"key":"806_CR63","doi-asserted-by":"crossref","unstructured":"Ke, X., Pettersson, P., Sierszecki, K., Angelov, C.: Verification of COMDES-II systems using UPPAAL with model transformation. In: 2008 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pp.\u00a0153\u2013160 (2008)","DOI":"10.1109\/RTCSA.2008.32"},{"key":"806_CR64","unstructured":"Bure\u0161, T., Carlson, J., Crnkovic, I., Sentilles, S., Vulgarakis, A.: ProCom: the progress component model reference manual. M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden (2008)"},{"key":"806_CR65","doi-asserted-by":"crossref","unstructured":"Vulgarakis, A., Suryadevara, J., Carlson, J., Seceleanu, C., Pettersson, P.: Formal semantics of the ProCom real-time component model. In: 2009 35th Euromicro Conference on Software Engineering and Advanced Applications, IEEE, pp.\u00a0478\u2013485 (2009)","DOI":"10.1109\/SEAA.2009.53"},{"key":"806_CR66","doi-asserted-by":"crossref","unstructured":"Borde, E., Carlson, J.: Towards verified synthesis of ProCom, a component model for real-time embedded systems. In: Proceedings of the 14th International ACM Sigsoft Symposium on Component Based Software Engineering, pp.\u00a0129\u2013138 (2011)","DOI":"10.1145\/2000229.2000248"},{"key":"806_CR67","unstructured":"T\u00f3th, T., Hajdu, A., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: Stewart, D., Weissenbacher, G. (eds.), Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00806-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00806-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00806-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T02:44:14Z","timestamp":1625107454000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00806-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,1]]},"references-count":67,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["806"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00806-5","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7,1]]},"assertion":[{"value":"16 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 May 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 May 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 July 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}