Skip to main content
SpringerLink
Log in

Implementation of a toolset for prototyping algebraic specifications of concurrent systems

  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 632))

Included in the following conference series:

  • 117 Accesses

Abstract

We descrive some theoretical and practical aspects we had to solve while developing of a toolset to prototype (symbolically execute) algebraic specifications of concurrent, systems and languages. The methodology used in writing such specifications has allowed us to develop efficient specialized algorithms and strategies which we have implemented. The resulting prototype is being used as a research tool and its use, especially in conjunction with other existing verification tools, seems very promising.

Work partially supported by CNR-Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo, ESPRIT-BRA WG COMPASS and MURST 40%

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.

References

  1. E. Astesiano, A. Giovini, and G. Reggio. Algebraic specification at work. In T. Rus, editor, Proc. AMAST Conference, Berlin, 1992. Springer-Verlag.

    Google Scholar 

  2. E. Astesiano, F. Mazzanti, G. Reggio, and E. Zucca. Formal specification of a concurrent architecture in a real project. In A Broad Perspective of Current Developments, Proc. ICS'85 (ACM International Computing Symposium), pages 185–195, Amsterdam, 1985. North-Holland.

    Google Scholar 

  3. E. Astesiano, C. Bendix Nielsen, N. Botta, A. Fantechi, A. Giovini, P. Inverardi, E. Karlsen, F. Mazzanti, J. Storbank Pedersen, G. Reggio, and E. Zucca. The draft formal definition of ANSI/MIL-STD 1815a Ada. Deliverable 7, CEC-MAP project, 1986.

    Google Scholar 

  4. E. Astesiano and G. Reggio. Direct semantics for concurrent languages in the SMoLCS approach. IBM Journal of Research and Development, 31(5):512–534, 1987.

    Google Scholar 

  5. E. Astesiano and G. Reggio. SMoLCS-driven concurrent calculi. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proc. TAPSOFT'87, Vol. 1, sanumber 249 in Lecture Notes in Computer Science, pages 169–201, Berlin, 1987. Springer Verlag.

    Google Scholar 

  6. E. Astesiano and G. Reggio. A structural approach to the formal modelization and specification of concurrent systems. Technical Report 0, Formal Methods Group, Dipartimento di Matematica, Università di Genova, Italy, 1990.

    Google Scholar 

  7. J.A. Bergstra and J.W. Klop. Process algebra for for synchronous communication. Information & Control, 60(1/3):109–137, 1984.

    Google Scholar 

  8. D. Bertello. Specifica di un sistema idroelettrico con metodi formali algebrici. Master's thesis, Universitá di Genova, 1991. (in italian).

    Google Scholar 

  9. T. Bolognesi and M. Caneve. Squiggles: a tool for the analysis of lotos specifications. In K. Turner, editor, Formal Description Techniques, pages 201–216. North-Holland, 1989.

    Google Scholar 

  10. A. Capani. Fondamenti algebrici, design e implementazione di un sistema di prototipazione rapida di specifiche di linguaggi e di sistemi concorrenti. Master's thesis, Universitá di Genova, 1992. (in italian).

    Google Scholar 

  11. R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In Proc. Workshop on erification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 1–20, Berlin, 1990. Springer-Verlag.

    Google Scholar 

  12. R. de Simone and D. Vergamini. Aboard auto. Technical Report 111, INRIA, 1989.

    Google Scholar 

  13. A. Giovini and F. Morando. SMoLCS/RP: a rapid prototyping tool for separable relational specifications. Technical report, Dipartimento di Matematica, Università di Genova, Italy, 1987.

    Google Scholar 

  14. J.C. Godskesen, K.G. Larsen, and M. Zeeberg. Tav user's manual. Internal report, Aalborg University Center, 1989.

    Google Scholar 

  15. H. Hussman. Rapid prototyping for algebraic specifications — RAP system user's manual. Technical Report MIP-8504, University of Passau, 1985. (second edition).

    Google Scholar 

  16. H. Hussman. Unification in conditional equational theories. In Proc. EUROCAL'85, number 204 in Lecture Notes in Computer Science, Berlin, 1985. Springer Verlag.

    Google Scholar 

  17. H. Lin. Pam: A process algebra manipulator. Internal Report 2/91, University of Sussex, 1991.

    Google Scholar 

  18. R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 120–1242. Elsevier, 1990.

    Google Scholar 

  19. F. Morando. Un interprete per specifiche di sistemi concorrenti secondo la metodologia SMoLCS. Master's thesis, Universitá di Genova, 1986. (in italian).

    Google Scholar 

  20. A. Morgavi. Specifica di una stazione ad alta tensione con metodi formali algebrici. Master's thesis, Universitá di Genova, 1992. (in italian).

    Google Scholar 

  21. G. Plotkin. A structural approach to operational semantics. Lecture notes, Aarhus University, 1981.

    Google Scholar 

  22. G. Reggio. Una metodologia per la specifica di sistemi e linguaggi concorrenti. PhD thesis, Universitá di Genova-Pisa-Udine, 1988. (in italian).

    Google Scholar 

  23. G. Reggio. Formal specification of a lift system. In Proc. of 2nd Magrabian Conference, 1992.

    Google Scholar 

  24. B. Thomsen. A calculus of higher-order communicating systems. In Proceeding of POPL Conference, pages 143–154, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI, Dipartimento di Informatica e Scienze dell'Informazione Università di Genova, Italy

    Alessandro Giovini, Franco Morando & Antonio Capani

Authors
  1. Alessandro Giovini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Franco Morando
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antonio Capani
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hélène Kirchner Giorgio Levi

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Giovini, A., Morando, F., Capani, A. (1992). Implementation of a toolset for prototyping algebraic specifications of concurrent systems. In: Kirchner, H., Levi, G. (eds) Algebraic and Logic Programming. ALP 1992. Lecture Notes in Computer Science, vol 632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013836

Download citation

  • DOI: https://doi.org/10.1007/BFb0013836

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55873-6

  • Online ISBN: 978-3-540-47302-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation