Automata Describing Object Behavior

  • Bernhard Rumpe
  • Cornel Klein
Part of the The Springer International Series in Engineering and Computer Science book series (SECS, volume 371)


Relating formal refinement techniques with commercial object-oriented software development methods is important to achieve enhancement of the power and flexibility of these software development methods- and tools. We will present an automata model together with a denotational and an operational semantics to describe the behavior of objects. Based on the given semantics, we define a set of powerful refinement rules, and discuss their applicability in software engineering practice, especially with the use of inheritance.


Operational Semantic Abstract Syntax Description Technique Digital Equipment Corporation Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [A93]
    M. Abadi. Baby Modula-3 and a Theory of Objects. SRC Research Report 95, Digital Equipment Corporation, February 1993.Google Scholar
  2. [AC93]
    R. M. Amadio and L. Cardelli. Subtyping Recursive Types. SRC Research Report 62, Digital Equipment Corporation, January 1993.Google Scholar
  3. [AG90]
    C. Asworth and M. Goodland. SSADM — A practical approach. McGraw-Hill, 1990.Google Scholar
  4. [B94]
    G. Booch. Object Oriented Analysis and Design with Applications. Benjamin/Cummings Publishing Company, Inc., 1994.Google Scholar
  5. [B94a]
    M. Broy. SysLab — Projektbeschreibung. Internal project report, October 1994.Google Scholar
  6. [BDDFGW93]
    M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T. F. Gritzner, and R. Weber. The Design of Distributed Systems — An Introduction to FOCUS-revised version-. SFB-Bericht 342/2-2/92 A, Technische Universität München, January 1993.Google Scholar
  7. [BFGHHNRSS93]
    M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hu\mann, D. Nazareth, F. Regensburger, O. Slotosch, and K. Stølen. The Requirement and Design Specification Language Spectrum, An Informal Introduction, Version 1.0, Part 1. Technical Report TUM-I9312, Technische Universität München, 1993.Google Scholar
  8. [BHS96]
    M. Broy, H. Hu\mann, and B. Schätz. Graphical Development of Consistent System Specifications. In FME’96, Formal Methods Europe, Symposium’ 96, LNCS. Springer-Verlag, Berlin, 3 1996, to appear.Google Scholar
  9. [C76]
    P.P. Chen. The Entity-Relationship Model — Towards a Unified View of Data. ACM Transactions on Database Systems, l(1):9–36, 1976.CrossRefGoogle Scholar
  10. [C93]
    L. Cardelli. Extensible Records in a Pure Calculus of Subtyping. SRC Research Report 81, Digital Equipement Corporation, January 1993.Google Scholar
  11. [CABDGHJ94]
    D. Coleman, P. Arnold, S. Bodoff, C. Dollin, H. Gilchrist, F. Hayes, and P. Jeremaes. Object-Oriented Development: The Fusion Method. Prentice Hall, 1994.Google Scholar
  12. [CDGJKN92]
    L. Cardelli, J. Donahue, L. Glassman, M. Jordan, B. Kalsow, and G. Nelson. Modula-3 Language Definition. ACM SIGPLAN NOTICES, 27(8):15–42, August 1992.CrossRefGoogle Scholar
  13. [F95]
    C. Facchi. Methodik zur formalen Spezifikation des ISO/OSI Schichtenmod-ells. Herbert Utz Verlag Wissenschaft, 1995. PhD Thesis.Google Scholar
  14. [H85]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  15. [H87]
    D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231–274, 1987.MATHCrossRefMathSciNetGoogle Scholar
  16. [H93]
    R. Hettler. Zur Übersetzung von E/R-Schemata nach SPECTRUM. Technical Report TUM-I9333, Technische Universität München, 1993.Google Scholar
  17. [H94]
    H. Hu\mann. Formal Foundations for SSADM. Technische Universität München, Habilitation Thesis, 1994.Google Scholar
  18. [H95]
    R. Hettler. Entity/Relationship-Datenmodellierung in axiomatischen Spez-ifikationssprachen. Tectum Verlag, München, 1995. PhD Thesis.Google Scholar
  19. [HL93]
    H.J. Habermann and F. Leymann. Repository—eine Einfuhrung. Handbuch der Informatik. Oldenbourg, 1993.Google Scholar
  20. [HM93]
    A. Hevner and H. Mills. Box-Structured Methods for Systems Development with Objects. IBM Systems Journal, 2:232–251, 1993.CrossRefGoogle Scholar
  21. [HU90]
    J. Hopcroft and J. Ullman. Einführung in die Autornatentheorie, Formale Sprachen und Komplexitdtstheorie. Addison-Wesley, 1990.Google Scholar
  22. [J85]
    B. Jonsson. A Model and Proof System for Asynchronous Networks. In Proc. 4th ACM Symposium on Principles of Distributed Computing. ACM, 1985.Google Scholar
  23. [J87]
    B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Uppsala University, Uppsala Sweden, 1987.Google Scholar
  24. [J93]
    I. Jacobson. Object-Oriented Software Engineering — a Use Case Driven Approach. Addison Wesley, 1993.Google Scholar
  25. [J93a]
    R. Janicki. Towards a Formal Semantics of Tables. Technical Report 264, CRL, September 1993.Google Scholar
  26. [L91]
    L. Lamport. The temporal logic of actions. Technical Report 79, Digital Equipment Corporation, Systems Research Center, Palo Alto, California, December 1991.Google Scholar
  27. [LS89]
    N. Lynch and E. Stark. A Proof of the Kahn Principle for Input/Output Automata. Information and Computation, 82:81–92, 1989.MATHCrossRefMathSciNetGoogle Scholar
  28. [LW93]
    B. Liskov and J. M. Wing. A New Definition of the Subtype Relation. In ECOOP 93, pages 118–141, 1993.Google Scholar
  29. [M89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  30. [MDL87]
    H. Mills, M. Dyer, and R. Linger. Cleanroom Software Engineering. IEEE Software, 4:19–24, 1987.CrossRefGoogle Scholar
  31. [N93]
    O. Nierstrasz. Regular Types for Active Objects. In Andreas Paepke, editor, OOPSLA’ 93. ACM Press, October 1993.Google Scholar
  32. [N93a]
    F. Nickl. Ablaufspezifikation durch Datenflu\modellierung und stromverar-beitende Funktionen. Technical Report TUM-I9334, Technische Universität München, 1993.Google Scholar
  33. [P92]
    C. Parnas. Tabular Representation of Relations. Technical Report 260, CRL, October 1992.Google Scholar
  34. [P95]
    M. Petre. Why Looking Isn’t Always Seeing: Readership Skills and Graphical Programming. Communications of the ACM, 38(6):33–44, June 1995.CrossRefGoogle Scholar
  35. [PR94]
    B. Paech and B. Rumpe. A new Concept of Refinement used for Behaviour Modelling with Automata. In FME’94, Formal Methods Europe, Symposium’ 94, LNCS 873. Springer-Verlag, Berlin, October 1994.Google Scholar
  36. [PR94b]
    B. Paech and B. Rumpe. Spezifikationsautomaten: Eine Erweiterung der Spezifikationssprache Spectrum um eine graphische Notation. In Formale Grundlagen für den Entwurf von Informationssystemen, GI-Workshop, Tutzing 24.–26. Mai 1994 (GI FG 2.5.2 EMISA). Institut für Informatik, Universität Hannover, May 1994.Google Scholar
  37. [R94]
    B. Rumpe. Verwendung endlicher Automaten zur Implementierung des dy-namischen Verhaltens von C++ Objekten. In G. Snelting U. Meyer, editor, Semantikgestuetzte Analyse, Entwicklung und Generierung von Program-men, 9402. Justus-Liebig-Universität Giessen, March 1994.Google Scholar
  38. [R96]
    B. Rumpe. Formale Methodik für den Entwurj verteilter objektorientierter Systeme. Phd-thesis, to appear, Technische Universität München, 1996.Google Scholar
  39. [RBPEL91]
    J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-Oriented Modeling and Design. Prentice Hall, 1991.Google Scholar
  40. [RKB95]
    B. Rumpe, C. Klein, and M. Broy. Ein strombasiertes mathematisches Modell verteilter informationsverarbeitender Systeme — Syslab Systemmodell —. Technical Report TUM-I9510, Technische Universität München, Institut für Informatik, March 1995.Google Scholar
  41. [S91]
    B. Stroustrup. The C++ Programming Language. Addison-Wesley, 1991.Google Scholar
  42. [S94]
    K. Spies. Funktionale Spezifikation eines Kommunikationsprotokolls. SFB-Bericht 342/08/94 A, Technische Universität München, Mai 1994.Google Scholar
  43. [SFD92]
    L.T. Semmens, R.B. France, and T.W.G. Docker. Integrated Structued Analysis and Formal Specification Techniques. The Computer Journal, 35(6):600–610, 1992.CrossRefGoogle Scholar
  44. [SM92]
    S. Shlaer and S. Mellor. Object Lifecycles, Modeling the World in States. Yourdon Press, 1992.Google Scholar
  45. [T89]
    I. Thomas. PCTE interfaces: Supporting tools in software-engineering environments. IEEE Software, pages 15–23, November 1989.Google Scholar
  46. [T90]
    W. Thomas. Automata on Infinite Objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume Band B, chapter 4, pages 135–192. Elsevier Publisher Amsterdam, 1990.Google Scholar
  47. [W90]
    Peter Wegner. Concepts and Paradigms of Object-Oriented Programming. OOPS Messenger, l(1):7–87, 1990.CrossRefGoogle Scholar
  48. [WZ88]
    P. Wegner and S. Zdonik. Inheritance as an Incremental Modification Mechanism or What Like Is and Isn’t Like. In S. Gjessing and K. Nygaard, editors, Proceedings ECOOP’ 88, LNCS 322, pages 55-77. Springer Verlag, Oslo, August 1988.Google Scholar

Copyright information

© Kluwer Academic Publishers 1996

Authors and Affiliations

  • Bernhard Rumpe
    • 1
  • Cornel Klein
    • 1
  1. 1.Institut für InformatikTechnische Unversität MünchenMünchenGermany

Personalised recommendations