Skip to main content
SpringerLink
Log in

A metalanguage for the formal requirement specification of reactive systems

  • Papers
  • Conference paper
  • First Online:
FME '93: Industrial-Strength Formal Methods (FME 1993)

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

Included in the following conference series:

Abstract

The essential novelty of what we have presented lies in the possibility of specifying within the same formalism requirements about the static structure and the dynamic activity of a system.

Compared to the many formalisms using various forms of temporal logics, we have two distinguished features: the possibility of dealing both with different entities (of different sorts) and with the subcomponents of an entity, without lowering the abstraction level of a specification; moreover our formalism includes the usual specifications of abstract data types and it allows also to give integrate specifications of the dynamic and of the static features of a system.

The formalism has a clean mathematical support in the definition of an appropriate institution; to this end a key role is played by the definition of the class of models, which are entity algebras over extended signatures.

There is no room here for illustrating the possibility of relating such abstract requirement specifications to the design level specifications (e.g. the SMoLCS specifications of [2]); this can be done following an algebraic approach based on a notion of implementation, due to Sannella-Wirsing [22] (see [8, 4] for some examples).

Finally it may be of interest to mention the fact that the approach presented here is currently being used in some industrial case studies for relating requirements to more concrete design specifications, which have been already given (see Section 5.2).

This work has been supported by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo” of C.N.R. (Italy), Esprit-BRA W.G. COMPASS n. 6112 and by a grant ENEL-SPA/CRA (Milano Italy).

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, G.F. Mascari, G. Reggio, and M. Wirsing. On the parameterized algebraic specification of concurrent systems. In H. Ehrig, C. Floyd, M. Nivat, and J. Thatcher, editors, Proc. TAPSOFT'85, Vol. 1, number 185 in Lecture Notes in Computer Science, pages 342–358. Springer Verlag, Berlin, 1985.

    Google Scholar 

  2. 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, number 249 in Lecture Notes in Computer Science, pages 169–201. Springer Verlag, Berlin, 1987.

    Google Scholar 

  3. E. Astesiano and G. Reggio. Algebraic specification of concurrency (invited lecture). In Recent Trends in Data Type Specification, number 655 in Lecture Notes in Computer Science. Springer Verlag, Berlin, 1992.

    Google Scholar 

  4. E. Astesiano and G. Reggio. Entity institutions: Frameworks for dynamic systems, 1992. in preparation.

    Google Scholar 

  5. E. Astesiano and G. Reggio. A structural approach to the formal modelization and specification of concurrent systems. Technical Report PDISI-92-01, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, Italy, 1992.

    Google Scholar 

  6. R.M. Burstall and J.A. Goguen. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programming Workshop, number 164 in Lecture Notes in Computer Science, pages 221–255. Springer Verlag, Berlin, 1984.

    Google Scholar 

  7. M. Cerioli and G. Reggio. Institutions for very abstract specifications. Technical Report PDISI-92-14, Dipartimento di Informatica e Scienze dell'informazione — Università di Genova, Italy, 1992.

    Google Scholar 

  8. G. Costa and G. Reggio. Abstract dynamic data types: a temporal logic approach. In A. Tarlecki, editor, Proc. MFCS'91, number 520 in Lecture Notes in Computer Science, pages 103–112. Springer Verlag, Berlin, 1991.

    Google Scholar 

  9. J. Fiadeiro and T. Maibaum. Describing, structuring and implementing objects. In J.W. de Bakker, W. P. de Roever, and G. Rozemberg, editors, Foundations of Object-Oriented Languages, Proc. REX School/Workshoop, number 489 in Lecture Notes in Computer Science, pages 274–310. Springer Verlag, Berlin, 1991.

    Google Scholar 

  10. I.S.O. LOTOS — A formal description technique based on the temporal ordering of observational behaviour. IS 8807, International Organization for Standardization, 1989.

    Google Scholar 

  11. L. Lamport. Specifying concurrent program modules. ACM TOPLAS, (5), 1983.

    Google Scholar 

  12. S. Mauw and G. J. Veltink. An introduction to PSFd. In J. Diaz and F. Orejas, editors, Proc. TAPSOFT'89, Vol. 2, number 352 in Lecture Notes in Computer Science, pages 272–285. Springer Verlag, Berlin, 1989.

    Google Scholar 

  13. R. Milner. A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer Verlag, Berlin, 1980.

    Google Scholar 

  14. G. Plotkin. An operational semantics for CSP. In D. Bjorner, editor, Proc. IFIP TC 2-Working conference: Formal description of programming concepts, pages 199–223. North-Holland, Amsterdam, 1983.

    Google Scholar 

  15. A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In Current Trends in Concurrency, number 224 in Lecture Notes in Computer Science, pages 510–584. Springer Verlag, Berlin, 1986.

    Google Scholar 

  16. G. Reggio. Entities: an istitution for dynamic systems. In H. Ehrig, K.P. Jantke, F. Orejas, and H. Reichel, editors, Recent Trends in Data Type Specification, number 534 in Lecture Notes in Computer Science, pages 244–265. Springer Verlag, Berlin, 1991.

    Google Scholar 

  17. G. Reggio. Event logic for specifying abstract dynamic data types. In Recent Trends in Data Type Specification, number 655 in Lecture Notes in Computer Science. Springer Verlag, Berlin, 1992.

    Google Scholar 

  18. G. Reggio, D. Bertello, and E. Crivelli. Specification of a hydro-electric central. Technical Report PDISI-92-13, Dipartimento di Informatica e Scienze dell'Informazione — Università di Genova, Italy, 1992.

    Google Scholar 

  19. G. Reggio, A. Morgavi, and V. Filippi. Specification of a high-voltage substation. Technical Report PDISI-92-12, Dipartimento di Informatica e Scienze dell'Informazione — Università di Genova, Italy, 1992.

    Google Scholar 

  20. W. Reisig. Petri nets: an introduction. Number 4 in EATCS Monographs on Theoretical Computer Science. Springer Verlag, Berlin, 1985.

    Google Scholar 

  21. C. Stirling. Comparing linear and branching time temporal logics. In Temporal logics of Specification, number 398 in Lecture Notes in Computer Science. Springer Verlag, Berlin, 1989.

    Google Scholar 

  22. M. Wirsing. Algebraic specifications. In van Leeuwen Jan, editor, Handbook of Theoret. Comput. Sci., volume B, pages 675–788. Elsevier, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, Viale Benedetto XV, 3, 16132, 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

James C. P. Woodcock Peter G. Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Astesiano, E., Reggio, G. (1993). A metalanguage for the formal requirement specification of reactive systems. In: Woodcock, J.C.P., Larsen, P.G. (eds) FME '93: Industrial-Strength Formal Methods. FME 1993. Lecture Notes in Computer Science, vol 670. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024642

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56662-5

  • Online ISBN: 978-3-540-47623-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation