{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:22:53Z","timestamp":1725988973309},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030002435"},{"type":"electronic","value":"9783030002442"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00244-2_14","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T00:12:38Z","timestamp":1535587958000},"page":"211-222","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Note on Refinement in Hierarchical Transition Systems"],"prefix":"10.1007","author":[{"given":"Gerald","family":"L\u00fcttgen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/FSE, pp. 109\u2013120. ACM (2001)","DOI":"10.1145\/503209.503226"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-25929-6_1","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"A Basu","year":"2012","unstructured":"Basu, A., Bensalem, S., Bozga, M., Bourgos, P., Sifakis, J.: Rigorous system design: the BIP approach. In: Kot\u00e1sek, Z., Bouda, J., \u010cern\u00e1, I., Sekanina, L., Vojnar, T., Anto\u0161, D. (eds.) MEMICS 2011. LNCS, vol. 7119, pp. 1\u201319. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-25929-6_1"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-12002-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SS Bauer","year":"2010","unstructured":"Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175\u2013189. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_15"},{"issue":"2\u20133","key":"14_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electron. Des. Autom."},{"issue":"C","key":"14_CR5","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.tcs.2016.06.011","volume":"642","author":"F Bujtor","year":"2016","unstructured":"Bujtor, F., Fendrich, S., L\u00fcttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theoret. Comput. Sci. 642(C), 24\u201353 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Drusinsky, D.: Modeling and Verification Using UML Statecharts. Newnes (2006)","DOI":"10.1016\/B978-075067949-7\/50004-0"},{"issue":"3","key":"14_CR7","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":"14_CR8","doi-asserted-by":"publisher","unstructured":"Fendrich, S., L\u00fcttgen, G.: A generalised theory of interface automata, component compatibility and error. Acta Inf. (2018). https:\/\/doi.org\/10.1007\/s00236-018-0319-8","DOI":"10.1007\/s00236-018-0319-8"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-030-00244-2_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2018","unstructured":"Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189\u2013210. Springer, Cham (2018)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0039066","volume-title":"CONCUR 1990 Theories of Concurrency: Unification and Extension","author":"RJ Glabbeek","year":"1990","unstructured":"Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278\u2013297. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039066"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-73196-2_1","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007","author":"S Graf","year":"2007","unstructured":"Graf, S., Quinton, S.: Contracts for BIP: hierarchical interaction models for compositional verification. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 1\u201318. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73196-2_1"},{"issue":"5","key":"14_CR12","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. Comput. 8(5), 607\u2013616 (1996)","journal-title":"Formal Asp. Comput."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-16901-4_29","volume-title":"Formal Methods and Software Engineering","author":"I Ben-Hafaiedh","year":"2010","unstructured":"Ben-Hafaiedh, I., Graf, S., Quinton, S.: Reasoning about safety and progress using contracts. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 436\u2013451. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16901-4_29"},{"issue":"5\u20136","key":"14_CR14","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-007-0049-7","volume":"9","author":"G Hamon","year":"2007","unstructured":"Hamon, G., Rushby, J.M.: An operational semantics for Stateflow. STTT 9(5\u20136), 447\u2013456 (2007)","journal-title":"STTT"},{"key":"14_CR15","unstructured":"Harbird, L.: Patterns and Model Transformation Tools for Designing Contractual State Machines. Ph.D thesis, Univ. York, UK (2011)"},{"key":"14_CR16","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."},{"issue":"4","key":"14_CR17","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."},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) Computer Aided Verification. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_19"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"L\u00fcttgen, G., von der Beeck, M., Cleaveland, R.: A compositional approach to Statecharts semantics. In: FSE, ACM Software Engineering Notes, vol. 25(6), pp. 120\u2013129. ACM (2000)","DOI":"10.1145\/355045.355062"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-63875-X_52","volume-title":"Advances in Computing Science \u2014 ASIAN\u201997","author":"E Mikk","year":"1997","unstructured":"Mikk, E., Lakhnechi, Y., Siegel, M.: Hierarchical automata as model for Statecharts. In: Shyamasundar, R.K., Ueda, K. (eds.) ASIAN 1997. LNCS, vol. 1345, pp. 181\u2013196. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63875-X_52"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-54415-1_49","volume-title":"Theoretical Aspects of Computer Software","author":"A Pnueli","year":"1991","unstructured":"Pnueli, A., Shalev, M.: What is in a step: on the semantics of Statecharts. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 244\u2013264. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54415-1_49"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Quinton, S., Graf, S.: Contract-based verification of hierarchical systems of components. In: SEFM, pp. 377\u2013381. IEEE (2008)","DOI":"10.1109\/SEFM.2008.28"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-13754-9_15","volume-title":"Time for Verification","author":"W-P Roever de","year":"2010","unstructured":"de Roever, W.-P., L\u00fcttgen, G., Mendler, M.: What Is in a step: new perspectives on a classical question. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 370\u2013399. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_15"},{"key":"14_CR24","unstructured":"Schmidt, H.: On the Role of Nondeterminism and Refinement in Model-Driven Top-Down Development of Software Systems. Ph.D thesis, Univ. Kiel, Germany (2009)"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-030-00244-2_15","volume-title":"Formal Methods for Industrial Critical Systems","author":"B Steffen","year":"2018","unstructured":"Steffen, B., Murtovi, A.: M3C: modal meta model checking. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 223\u2013241. Springer, Cham (2018)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00244-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T02:02:43Z","timestamp":1571796163000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00244-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002435","9783030002442"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00244-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}