Abstract
This paper presents ABS, an abstract behavioral specification language for designing executable models of distributed object-oriented systems. The language combines advanced concurrency and synchronization mechanisms for concurrent object groups with a functional language for modeling data. ABS uses asynchronous method calls, interfaces for encapsulation, and cooperative scheduling of method activations inside concurrent objects. This feature combination results in a concurrent object-oriented model which is inherently compositional. We discuss central design issues for ABS and formalize the type system and semantics of Core ABS, a calculus with the main features of ABS. For Core ABS, we prove a subject reduction property which shows that well-typedness is preserved during execution; in particular, “method not understood” errors do not occur at runtime for well-typed ABS models. Finally, we briefly discuss the tool support developed for ABS.
Partly funded by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using Formal Models ( http://www.hats-project.eu ).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Agha, G.A.: ACTORS: A Model of Concurrent Computations in Distributed Systems. The MIT Press, Cambridge (1986)
Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Science of Computer Programming (2010) (In press)
Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Reading (2000)
Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf (2007)
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. 3362, pp. 49–69. Springer, Heidelberg (2005)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3) (June 2004)
Cardelli, L.: A language with distributed scope. Comp. Sys. 8(1), 27–59 (1995)
Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous sequential processes. Information and Computation 207(4), 459–495 (2009)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Clements, P.C.: A survey of architecture description languages. In: Proc. Workshop on Software Specification and Design (IWSSD 1996), pp. 16–25. IEEE, Los Alamitos (1996)
Dahl, O.-J.: Monitors revisited. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 93–103. Prentice Hall, Englewood Cliffs (1994)
de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)
Full ABS Modeling Framework, Deliverable 1.2 of project FP7-231620 (HATS) (March 2011), http://www.hats-project.eu
Verification of Behavioral Properties, Deliverable 2.5 of project FP7-231620 (HATS) (March 2011), http://www.hats-project.eu
Di Blasio, P., Fisher, K.: A calculus for concurrent objects. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 655–670. Springer, Heidelberg (1996)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975)
Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of dynamic systems: Component reasoning for concurrent objects. In: Proc. Foundations of Interactive Computation (FInCo 2007). ENTCS, vol. 203, pp. 19–34. Elsevier, Amsterdam (2008)
Ekman, T., Hedin, G.: The JastAdd system: modular extensible compiler construction. Science of Computer Programming 69(1-3), 14–26 (2007)
Gordon, A.D., Hankin, P.D.: A concurrent object calculus: Reduction and typing. In: Proc. High-Level Concurrent Languages (HLCL). ENTCS, vol. 16(3) (1998)
Haller, P., Odersky, M.: Scala actors: Unifying thread-based and event-based programming. Theor. Comp. Sci. 410(2-3), 202–220 (2009)
Hoare, C.A.R.: Monitors: an operating systems structuring concept. Communications of the ACM 17(10), 549–557 (1974)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. and Sys 23(3), 396–450 (2001)
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 35–58 (2007)
Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theor. Comp. Sci. 365(1-2), 23–66 (2006)
Johnsen, E.B., Yu, I.C.: Backwards type analysis of asynchronous method calls. Journal of Logic and Algebraic Programming 77, 40–59 (2008)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer (STTT) 1(1-2), 134–152 (1997)
Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proc. POPL, pp. 47–57. ACM Press, New York (1988)
Magee, J., Dulay, N., Eisenbach, S., Kramer, J.: Specifying distributed software architectures. In: Botella, P., Schäfer, W. (eds.) ESEC 1995. LNCS, vol. 989, pp. 137–153. Springer, Heidelberg (1995)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comp. Sci. 96, 73–155 (1992)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
Pierce, B.C.: Types and Programming Languages. The MIT Press, Cambridge (2002)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)
Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275–299. Springer, Heidelberg (2010)
van Deursen, A., Klint, P.: Domain-specific language design requires feature descriptions. Journal of Computing and Information Technology 10(1), 1–18 (2002)
Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modelling with UML. Object Technology Series. Addison-Wesley, Reading (1999)
Welc, A., Jagannathan, S., Hosking, A.: Safe futures for Java. In: Proc. OOPSLA, pp. 439–453. ACM, New York (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M. (2011). ABS: A Core Language for Abstract Behavioral Specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds) Formal Methods for Components and Objects. FMCO 2010. Lecture Notes in Computer Science, vol 6957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25271-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-25271-6_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25270-9
Online ISBN: 978-3-642-25271-6
eBook Packages: Computer ScienceComputer Science (R0)