{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T19:32:03Z","timestamp":1774121523411,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642406140","type":"print"},{"value":"9783642406157","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40615-7_1","type":"book-chapter","created":{"date-parts":[[2013,8,21]],"date-time":"2013-08-21T21:08:02Z","timestamp":1377119282000},"page":"1-37","source":"Crossref","is-referenced-by-count":31,"title":["The Abstract Behavioral Specification Language: A Tutorial Introduction"],"prefix":"10.1007","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"1_CR2","unstructured":"The ABS Language Specification, ABS version 1.2.0 edn. (April 2013), \n                  \n                    http:\/\/tools.hats-project.eu\/download\/absrefmanual.pdf\n                  \n                  \n                ."},{"issue":"12","key":"1_CR3","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.1016\/j.scico.2010.08.003","volume":"77","author":"W. Ahrendt","year":"2012","unstructured":"Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Science of Computer Programming\u00a077(12), 1289\u20131309 (2012)","journal-title":"Science of Computer Programming"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/978-3-642-40615-7_4","volume-title":"FMCO 2012","author":"E. Albert","year":"2013","unstructured":"Albert, E., et al.: Automatic inference of bounds on resource consumption. In: de Boer, F., Bonsangue, M., Giachino, E., H\u00e4hnle, R. (eds.) FMCO 2012. LNCS, vol.\u00a07866, pp. 119\u2013144. Springer, Heidelberg (2013)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Amighi, A., Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: The VerCors project: setting up basecamp. In: Claessen, K., Swamy, N. (eds.) Proc. Sixth Workshop on Programming Languages Meets Program Verification, PLPV, Philadelphia, PA, USA, pp. 71\u201382. ACM (2012)","DOI":"10.1145\/2103776.2103785"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21455-4_13","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"D. Clarke","year":"2011","unstructured":"Clarke, D., Diakov, N., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I., Sch\u00e4fer, J., Schlatte, R., Wong, P.Y.H.: Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol.\u00a06659, pp. 417\u2013457. Springer, Heidelberg (2011)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-25271-6_11","volume-title":"Formal Methods for Components and Objects","author":"D. Clarke","year":"2011","unstructured":"Clarke, D., Muschevici, R., Proen\u00e7a, J., Schaefer, I., Schlatte, R.: Variability modelling in the ABS language. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 204\u2013224. Springer, Heidelberg (2011)"},{"issue":"12","key":"1_CR10","doi-asserted-by":"publisher","first-page":"1130","DOI":"10.1016\/j.scico.2010.10.005","volume":"76","author":"A. Classen","year":"2011","unstructured":"Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: Syntax and semantics of TVL. Science of Computer Programming\u00a076(12), 1130\u20131143 (2011)","journal-title":"Science of Computer Programming"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A. Classen","year":"2012","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: Model checking software product lines with SNIP. International Journal on Software Tools for Technology Transfer (STTT)\u00a014, 589\u2013612 (2012)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-34026-0_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"F. Damiani","year":"2012","unstructured":"Damiani, F., Schaefer, I.: Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 193\u2013207. Springer, Heidelberg (2012)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-71316-6_22","volume-title":"Programming Languages and Systems","author":"F.S. Boer de","year":"2007","unstructured":"de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 316\u2013330. Springer, Heidelberg (2007)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35861-6_8","volume-title":"Formal Aspects of Component Software","author":"F.S. Boer de","year":"2013","unstructured":"de Boer, F.S., de Gouw, S.: Run-time verification of black-box components using behavioral specifications: An experience report on tool development. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol.\u00a07684, pp. 128\u2013133. Springer, Heidelberg (2013)"},{"key":"1_CR15","unstructured":"Report on the Core ABS Language and Methodology: Part A, Part of Deliverable 1.1 of project FP7-231620 (HATS) (March 2010), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR16","unstructured":"Final Report on Feature Selection and Integration, Deliverable 2.2b of project FP7-231620 (HATS) (March 2011), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR17","unstructured":"Full ABS Modeling Framework, Deliverable 1.2 of project FP7-231620 (HATS) (March 2011), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR18","unstructured":"Analysis Final Report, Deliverable 2.7 of project FP7-231620 (HATS) (December 2012), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR19","unstructured":"Evaluation of Modeling, Deliverable 5.3 of project FP7-231620 (HATS) (March 2012), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR20","unstructured":"Model Mining, Deliverable 3.2 of project FP7-231620 (HATS) (March 2012), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR21","unstructured":"Correctness, Deliverable 4.3 of project FP7-231620 (HATS) (March 2013), \n                  \n                    http:\/\/www.hats-project.eu"},{"key":"1_CR22","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-21461-5_11","volume-title":"Formal Techniques for Distributed Systems","author":"E. Giachino","year":"2011","unstructured":"Giachino, E., Laneve, C.: Analysis of deadlocks in object groups. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol.\u00a06722, pp. 168\u2013182. Springer, Heidelberg (2011)"},{"key":"1_CR24","volume-title":"Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications","author":"C. Girault","year":"2001","unstructured":"Girault, C., Valk, R.: Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications. Springer, Secaucus (2001)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-35887-6_6","volume-title":"Proc. 10th International Symposium on Formal Methods for Components and Objects (FMCO 2011)","author":"R. H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Helvensteijn, M., Johnsen, E.B., Lienhardt, M., Sangiorgi, D., Schaefer, I., Wong, P.Y.H.: HATS abstract behavioral specification: the architectural view. In: Beckert, B., Damiani, F., de Boer, F., Bonsangue, M.M. (eds.) FMCO 2011. LNCS, vol.\u00a07542, pp. 109\u2013132. Springer, Heidelberg (2013)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-34026-0_4","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"R. H\u00e4hnle","year":"2012","unstructured":"H\u00e4hnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 32\u201346. Springer, Heidelberg (2012)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-38574-2_21","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 300\u2013314. Springer, Heidelberg (2013)"},{"issue":"3","key":"1_CR28","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. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"1_CR29","first-page":"235","volume-title":"Proc. 3rd International Joint Conference on Artificial Intelligence","author":"C. Hewitt","year":"1973","unstructured":"Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for Artificial Intelligence. In: Nilsson, N.J. (ed.) Proc. 3rd International Joint Conference on Artificial Intelligence, pp. 235\u2013245. William Kaufmann, Stanford (1973)"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-642-40615-7_5","volume-title":"FMCO 2012","author":"E.B. Johnsen","year":"2013","unstructured":"Johnsen, E.B.: Separating cost and capacity for load balancing in ABS deployment models. In: de Boer, F., Bonsangue, M., Giachino, E., H\u00e4hnle, R. (eds.) FMCO 2012. LNCS, vol.\u00a07866, pp. 145\u2013167. Springer, Heidelberg (2013)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"E.B. Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 142\u2013164. Springer, Heidelberg (2011)"},{"issue":"1-2","key":"1_CR32","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2006.07.031","volume":"365","author":"E.B. Johnsen","year":"2006","unstructured":"Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theoretical Computer Science\u00a0365(1-2), 23\u201366 (2006)","journal-title":"Theoretical Computer Science"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-642-40615-7_3","volume-title":"FMCO 2012","author":"I.W. Kurnia","year":"2013","unstructured":"Kurnia, I.W., Poetzsch-Heffter, A.: Verification of open concurrent object systems. In: de Boer, F., Bonsangue, M., Giachino, E., H\u00e4hnle, R. (eds.) FMCO 2012. LNCS, vol.\u00a07866, pp. 83\u2013118. Springer, Heidelberg (2013)"},{"key":"1_CR34","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML Reference Manual. Draft revision 1.235 (September 2009)"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-34026-0_6","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"M. Lienhardt","year":"2012","unstructured":"Lienhardt, M., Bravetti, M., Sangiorgi, D.: An object group-based component model. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 64\u201378. Springer, Heidelberg (2012)"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-34026-0_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"M. Lienhardt","year":"2012","unstructured":"Lienhardt, M., Clarke, D.: Conflict detection in delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 178\u2013192. Springer, Heidelberg (2012)"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/0-387-97226-9_20","volume-title":"Hardware Specification, Verification and Synthesis: Mathematical Aspects","author":"G. Milne","year":"1990","unstructured":"Milne, G.: Design for verifiability. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol.\u00a0408, pp. 1\u201313. Springer, Heidelberg (1990)"},{"issue":"1","key":"1_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, J.: A calculus of mobile processes, I and II. Inform. and Comput.\u00a0100(1), 1\u201340, 41\u201377 (1992)","journal-title":"Inform. and Comput."},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Nobakht, B., de Boer, F.S., Jaghoori, M.M., Schlatte, R.: Programming and deployment of active objects with application-level scheduling. In: Proceedings of the 2012 ACM Symposium on Applied Computing (SAC). ACM (2012)","DOI":"10.1145\/2245276.2232086"},{"key":"1_CR40","unstructured":"Peyton Jones, S. (ed.): Haskell 98 Language and Libraries: The Revised Report (September 2002), \n                  \n                    http:\/\/haskell.org\/"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Pohl, K., B\u00f6ckle, G., Van Der Linden, F.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer (2005)","DOI":"10.1007\/3-540-28901-1"},{"key":"1_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15579-6_6","volume-title":"Software Product Lines: Going Beyond","author":"I. Schaefer","year":"2010","unstructured":"Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol.\u00a06287, pp. 77\u201391. Springer, Heidelberg (2010)"},{"key":"1_CR43","unstructured":"Schaefer, I., Worret, A., Poetzsch-Heffter, A.: A Model-Based Framework for Automated Product Derivation. In: Proc. of Workshop in Model-based Approaches for Product Line Engineering, MAPLE 2009 (2009)"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-14107-2_13","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"J. Sch\u00e4fer","year":"2010","unstructured":"Sch\u00e4fer, J., Poetzsch-Heffter, A.: Jcobox: Generalizing active objects to concurrent components. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 275\u2013299. Springer, Heidelberg (2010)"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Schobbens, P., Heymans, P., Trigaux, J.: Feature diagrams: A survey and a formal semantics. In: 14th IEEE International Conference on Requirements Engineering, pp. 139\u2013148 (2006)","DOI":"10.1109\/RE.2006.23"},{"key":"1_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-642-40615-7_2","volume-title":"FMCO 2012","author":"M. Dooren van","year":"2013","unstructured":"van Dooren, M., Clarke, D., Jacobs, B.: Subobject-Oriented programming. In: de Boer, F., Bonsangue, M., Giachino, E., H\u00e4hnle, R. (eds.) FMCO 2012. LNCS, vol.\u00a07866, pp. 38\u201382. Springer, Heidelberg (2013)"},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-21952-8_15","volume-title":"Objects, Models, Components, Patterns","author":"Y. Welsch","year":"2011","unstructured":"Welsch, Y., Sch\u00e4fer, J.: Location types for safe distributed object-oriented programming. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol.\u00a06705, pp. 194\u2013210. Springer, Heidelberg (2011)"},{"issue":"5","key":"1_CR48","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/s10009-012-0250-1","volume":"14","author":"P.Y.H. Wong","year":"2012","unstructured":"Wong, P.Y.H., Albert, E., Muschevici, R., Proen\u00e7a, J., Sch\u00e4fer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. Journal on Software Tools for Technology Transfer\u00a014(5), 567\u2013588 (2012)","journal-title":"Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40615-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T15:22:25Z","timestamp":1558020145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40615-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642406140","9783642406157"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40615-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}