From Conditional Specifications to Interaction Charts | SpringerLink
Skip to main content
Springer Nature Link
Log in

From Conditional Specifications to Interaction Charts

A Journey from Formal to Visual Means to Model Behaviour

  • Chapter
Formal Methods in Software and Systems Modeling

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

  • 688 Accesses

Abstract

In this paper, addressing the classical problem of modelling the behaviour of a system, we present a paradigmatic journey from purely formal and textual techniques to derived visual notations, with a further attention first to code generation and finally to the incorporation into a standard notation such as the UML.

We show how starting from Casl positive conditional specifications with initial semantics of labelled transition systems, we can devise a new visual paradigm, the interaction charts, which are diagrams able to express both reactive and proactive/autonomous behaviour.

Then, we introduce the executable interaction charts, which are interaction charts with a special semantics, by which we try to ease the passage to code generation.

Finally, we present the interaction machines, which are essentially executable interaction charts in a notation that can be easily incorporated, as an extension, into the UML.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Astesiano, E., Giovini, A., Mazzanti, F., Reggio, G., Zucca, E.: The Ada Challenge for New Formal Semantic Techniques. In: Proc. of the Ada-Europe International Conference on Ada: Managing the Transition, Edimburgh, pp. 239–248. University Press, Cambridge (1986)

    Google Scholar 

  2. Astesiano, E., Reggio, G.: Formalism and Method. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 93–114. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  3. Astesiano, E., Reggio, G.: Formalism and Method. T.C.S 236(1,2), 3–34 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  4. Astesiano, E., Reggio, G.: Labelled Transition Logic: An Outline. Acta Informatica 37(11-12), 831–879 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  5. Astesiano, E., Reggio, G., Cerioli, M.: From Formal Techniques toWell-Founded Software Development Methods. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 132–150. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Bidoit, M., Mosses, P.D.: CASL User Manual, Introduction to Using the Common Algebraic Specification Language. In: Bidoit, M., Mosses, P.D. (eds.) CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Choppy, C., Reggio, G.: Towards a Formally Grounded Software Development Method. Technical Report DISI–TR–03–35, DISI, Università di Genova, Italy (2003), Available at ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio03a.pdf

  8. Coscia, E., Reggio, G.: JTN: A Java-targeted Graphic Formal Notation for Reactive and Concurrent Systems. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol. 1577, pp. 77–97. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Costa, G., Reggio, G.: Specification of Abstract Dynamic Data Types: A Temporal Logic Approach. T.C.S. 173(2), 513–554 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  10. Ehrig, H., Mahr, B.: A Decade of TAPSOFT: Aspects of Progress and Prospects in Theory and Practice of Software Development. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 3–24. Springer, Heidelberg (1995)

    Google Scholar 

  11. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Berlin (1980)

    Google Scholar 

  12. Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  13. OMG. UML Specification 1.3 (2000), Available at http://www.omg.org/docs/formal/00-03-01.pdf

  14. OMG. UML 2.0 OCL Specification (2003)

    Google Scholar 

  15. OMG. UML 2.0 Superstructure Specification (2003)

    Google Scholar 

  16. Plotkin, G.: An Operational Semantics for CSP. In: Bjorner, D. (ed.) Proc. IFIP TC 2-Working conference: Formal description of programming concepts. North-Holland, Amsterdam (1983)

    Google Scholar 

  17. Reggio, G., Astesiano, E., Choppy, C.: Casl-Ltl: A Casl Extension for Dynamic Reactive Systems Version 1.0– Summary. Technical Report DISI-TR-03-36, DISI – Università di Genova, Italy (2003), Available at ftp://ftp.disi.unige.it/person/ReggioG/ReggioEtAll03b.ps

  18. Reggio, G., Astesiano, E., Choppy, C., Hussmann, H.: Analysing UML Active Classes and Associated State Machines – A Lightweight Formal Approach. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 127. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Reggio, G., Cerioli, M., Astesiano, E.: Towards a Rigorous Semantics of UML Supporting its Multiview Approach. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, p. 171. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  20. Reggio, G., Larosa, M.: A Graphic Notation for Formal Specifications of Dynamic Systems. In: Fitzgerald, J., Jones, C.B. (eds.) FME 1997. LNCS, vol. 1313. Springer, Heidelberg (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI, Università di Genova, Italy

    Egidio Astesiano & Gianna Reggio

Authors
  1. Egidio Astesiano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gianna Reggio
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Bremen, P.O. Box 33 04 40, 28334, Bremen, Germany

    Hans-Jörg Kreowski

  2. Dipartimento di Informatica, Università di Pisa,  

    Ugo Montanari

  3. Dpto de L.S.I., Universitat Politècnica de Catalunya, Campus Nord, Mòdul Omega, Jordi Girona 1-3, 08034, Barcelona, Spain

    Fernando Orejas

  4. Leiden Center of Advanced Computer Science (LIACS), Leiden University, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

  5. Philipps-Universität Marburg, Germany

    Gabriele Taentzer

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Astesiano, E., Reggio, G. (2005). From Conditional Specifications to Interaction Charts. In: Kreowski, HJ., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds) Formal Methods in Software and Systems Modeling. Lecture Notes in Computer Science, vol 3393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31847-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-31847-7_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-24936-8

  • Online ISBN: 978-3-540-31847-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation