A framework for modular formal specification and verification

  • Pierre Michel
  • Virginie Wiels
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


This paper presents a specification formalism that combines temporal logic with actions and algebraic modules. This formalism allows to write modular specifications of complex systems and is supported by a tool. We show that we can also exploit the structure of the specification in order to realize modular verifications. It is applied to a telecommunication example.


Temporal Logic Linear Temporal Logic Interpretation Function Modular Specification Algebraic Signature 
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. 1.
    CNET — Note technique NT/PAA/TSA/4727. Specification de la fonction de selection et de diffusion de notifications, 1996.Google Scholar
  2. 2.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985. Equations and initial semantics.Google Scholar
  3. 3.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990. Modules specifications and constraints.Google Scholar
  4. 4.
    U. Engberg. Reasoning in the Temporal Logic of Actions. PhD thesis, Department of Computer Science, University of Aarhus, September 1995.Google Scholar
  5. 5.
    J. Fiadeiro and T. Maibaum. Temporal theories as modularisation units for concurrent system specification. Formal Aspects of Computing, 4(3):239–272, 1992.CrossRefGoogle Scholar
  6. 6.
    J. Fiadeiro and T. Maibaum. Design structures for object-based systems. In S. Goldsack and S.Kent, editors, Formal Methods and Object Technology. Springer-Verlag, 1996.Google Scholar
  7. 7.
    C. Ghezzi, D. Madrioli, and A. Morzenti. TRIO: A logic language for executable specifications of real-time systems. jss, 12(2), 1990.Google Scholar
  8. 8.
    ITU Draft Rec. G.851-01. Management of the transport network — Application of the RM-ODP framework, 1996. Study Group 15 Contribution.Google Scholar
  9. 9.
    ITU Rec. X.901, ISO DIS 10746-1. Reference Model of Open Distributed Processing-Part1: Overview and Guide to Use, 1994.Google Scholar
  10. 10.
    F. Kroger. Abstract modules: Combining algebraic and temporal logic specification means. Technique et Science Informatiques, 6(6), 1987.Google Scholar
  11. 11.
    L. Lamport. The Temporal Logic of Actions. Technical Report 79, SRC, 1992.Google Scholar
  12. 12.
    P. Michel and V.Wiels. Assistance au développement et à la maintenace de logiciels basée sur la composition. In Les logiciels de télécommunications, Actes des séminaires action scientifique France Telecom, mars 1997.Google Scholar
  13. 13.
    P. Michel and V. Wiels. Modular specification and validation of systems. In ECOOP Workshop on Proof Theory of Concurrent Object-Oriented Programming, July 1996.Google Scholar
  14. 14.
    P. Michel and V. Wiels. Un calcul de modules pour combiner les développements ascendants et descendants. In Journee Formalisation des Activites Concurrentes LAAS-CNRS, 1996.Google Scholar
  15. 15.
    D.E. Rydeheard and R.M. Burstall. Computational Category Theory. International Series in Computer Science. Prentice Hall, 1988.Google Scholar
  16. 16.
    J. Sauloy. A calculus of modules built on a kernel for categorical computations. unpublished.Google Scholar
  17. 17.
    C. Seguin and V. Wiels. Using a Logical and Categorical Approach for the Validation of Fault-tolerant Systems. In Proceedings of FME'96, volume 1051 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  18. 18.
    G. van Rossum. Python tutorial., 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Pierre Michel
    • 1
  • Virginie Wiels
    • 1
  1. 1.ONERA-CERTToulouse cedexFrance

Personalised recommendations