Skip to main content
SpringerLink
Log in

The Abstract Behavioral Specification Language: A Tutorial Introduction

  • Chapter
Formal Methods for Components and Objects (FMCO 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7866))

Included in the following conference series:

Abstract

ABS (for abstract behavioral specification) is a novel language for modeling feature-rich, distributed, object-oriented systems at an abstract, yet precise level. ABS has a clear and simple concurrency model that permits synchronous as well as actor-style asynchronous communication. ABS abstracts away from specific datatype or I/O implementations, but is a fully executable language and has code generators for Java, Scala, and Maude. ABS goes beyond conventional programming languages in two important aspects: first, it embeds architectural concepts such as components or feature hierarchies and allows to connect features with their implementation in terms of product families. In contrast to standard OO languages, code reuse in ABS is feature-based instead of inheritance-based. Second, ABS has a formal semantics and has been designed with formal analyzability in mind. This paper gives a tutorial introduction to ABS. We discuss all important design features, explain why they are present and how they are intended to be used.

Research 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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)

    Google Scholar 

  2. The ABS Language Specification, ABS version 1.2.0 edn. (April 2013), http://tools.hats-project.eu/download/absrefmanual.pdf .

  3. Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Science of Computer Programming 77(12), 1289–1309 (2012)

    Article  MATH  Google Scholar 

  4. Albert, E., et al.: Automatic inference of bounds on resource consumption. In: de Boer, F., Bonsangue, M., Giachino, E., Hähnle, R. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 119–144. Springer, Heidelberg (2013)

    Google Scholar 

  5. 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–82. ACM (2012)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer (2003)

    Google Scholar 

  8. Clarke, D., Diakov, N., Hähnle, R., Johnsen, E.B., Schaefer, I., Schäfer, 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. 6659, pp. 417–457. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Clarke, D., Muschevici, R., Proença, 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. 6957, pp. 204–224. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: Syntax and semantics of TVL. Science of Computer Programming 76(12), 1130–1143 (2011)

    Article  Google Scholar 

  11. 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) 14, 589–612 (2012)

    Article  Google Scholar 

  12. 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. 7609, pp. 193–207. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. 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ăsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 128–133. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Report on the Core ABS Language and Methodology: Part A, Part of Deliverable 1.1 of project FP7-231620 (HATS) (March 2010), http://www.hats-project.eu

  16. Final Report on Feature Selection and Integration, Deliverable 2.2b of project FP7-231620 (HATS) (March 2011), http://www.hats-project.eu

  17. Full ABS Modeling Framework, Deliverable 1.2 of project FP7-231620 (HATS) (March 2011), http://www.hats-project.eu

  18. Analysis Final Report, Deliverable 2.7 of project FP7-231620 (HATS) (December 2012), http://www.hats-project.eu

  19. Evaluation of Modeling, Deliverable 5.3 of project FP7-231620 (HATS) (March 2012), http://www.hats-project.eu

  20. Model Mining, Deliverable 3.2 of project FP7-231620 (HATS) (March 2012), http://www.hats-project.eu

  21. Correctness, Deliverable 4.3 of project FP7-231620 (HATS) (March 2013), http://www.hats-project.eu

  22. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)

    Google Scholar 

  23. Giachino, E., Laneve, C.: Analysis of deadlocks in object groups. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 168–182. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Girault, C., Valk, R.: Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications. Springer, Secaucus (2001)

    Google Scholar 

  25. Hähnle, 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. 7542, pp. 109–132. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Hähnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 32–46. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  27. Hähnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 300–314. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  28. Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  29. 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–245. William Kaufmann, Stanford (1973)

    Google Scholar 

  30. Johnsen, E.B.: Separating cost and capacity for load balancing in ABS deployment models. In: de Boer, F., Bonsangue, M., Giachino, E., Hähnle, R. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 145–167. Springer, Heidelberg (2013)

    Google Scholar 

  31. Johnsen, E.B., Hähnle, R., Schäfer, 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. 6957, pp. 142–164. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  32. Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theoretical Computer Science 365(1-2), 23–66 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  33. Kurnia, I.W., Poetzsch-Heffter, A.: Verification of open concurrent object systems. In: de Boer, F., Bonsangue, M., Giachino, E., Hähnle, R. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 83–118. Springer, Heidelberg (2013)

    Google Scholar 

  34. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML Reference Manual. Draft revision 1.235 (September 2009)

    Google Scholar 

  35. Lienhardt, M., Bravetti, M., Sangiorgi, D.: An object group-based component model. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 64–78. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  36. Lienhardt, M., Clarke, D.: Conflict detection in delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 178–192. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  37. Milne, G.: Design for verifiability. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol. 408, pp. 1–13. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  38. Milner, R., Parrow, J., Walker, J.: A calculus of mobile processes, I and II. Inform. and Comput. 100(1), 1–40, 41–77 (1992)

    Google Scholar 

  39. 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)

    Google Scholar 

  40. Peyton Jones, S. (ed.): Haskell 98 Language and Libraries: The Revised Report (September 2002), http://haskell.org/

  41. Pohl, K., Böckle, G., Van Der Linden, F.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer (2005)

    Google Scholar 

  42. 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. 6287, pp. 77–91. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  43. 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)

    Google Scholar 

  44. 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)

    Chapter  Google Scholar 

  45. Schobbens, P., Heymans, P., Trigaux, J.: Feature diagrams: A survey and a formal semantics. In: 14th IEEE International Conference on Requirements Engineering, pp. 139–148 (2006)

    Google Scholar 

  46. van Dooren, M., Clarke, D., Jacobs, B.: Subobject-Oriented programming. In: de Boer, F., Bonsangue, M., Giachino, E., Hähnle, R. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 38–82. Springer, Heidelberg (2013)

    Google Scholar 

  47. Welsch, Y., Schäfer, J.: Location types for safe distributed object-oriented programming. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 194–210. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  48. Wong, P.Y.H., Albert, E., Muschevici, R., Proença, J., Schäfer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. Journal on Software Tools for Technology Transfer 14(5), 567–588 (2012)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technische Universität Darmstadt, Germany

    Reiner Hähnle

Authors
  1. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Computer Science, University of Bologna, Mura Anteo Zamboni, 7, 40127, Bologna, Italy

    Elena Giachino

  2. Dept. of Computer Science, Technical University of Darmstadt, Hochschulstr. 10, 64289, Darmstadt, Germany

    Reiner Hähnle

  3. Centre for Mathematics and Computer Science, CWI, Science Park 123, 1098 XG, Amsterdam, The Netherlands

    Frank S. de Boer

  4. Leiden Institute of Advanced Computer Science (LIACS), Leiden University, P.O. Box 9512, 2300 RA, Leiden, The Netherlands

    Marcello M. Bonsangue

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Hähnle, R. (2013). The Abstract Behavioral Specification Language: A Tutorial Introduction. In: Giachino, E., Hähnle, R., de Boer, F.S., Bonsangue, M.M. (eds) Formal Methods for Components and Objects. FMCO 2012. Lecture Notes in Computer Science, vol 7866. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40615-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40615-7_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40614-0

  • Online ISBN: 978-3-642-40615-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation