Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
CNET — Note technique NT/PAA/TSA/4727. Specification de la fonction de selection et de diffusion de notifications, 1996.
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.
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.
U. Engberg. Reasoning in the Temporal Logic of Actions. PhD thesis, Department of Computer Science, University of Aarhus, September 1995.
J. Fiadeiro and T. Maibaum. Temporal theories as modularisation units for concurrent system specification. Formal Aspects of Computing, 4(3):239–272, 1992.
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.
C. Ghezzi, D. Madrioli, and A. Morzenti. TRIO: A logic language for executable specifications of real-time systems. jss, 12(2), 1990.
ITU Draft Rec. G.851-01. Management of the transport network — Application of the RM-ODP framework, 1996. Study Group 15 Contribution.
ITU Rec. X.901, ISO DIS 10746-1. Reference Model of Open Distributed Processing-Part1: Overview and Guide to Use, 1994.
F. Kroger. Abstract modules: Combining algebraic and temporal logic specification means. Technique et Science Informatiques, 6(6), 1987.
L. Lamport. The Temporal Logic of Actions. Technical Report 79, SRC, 1992.
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.
P. Michel and V. Wiels. Modular specification and validation of systems. In ECOOP Workshop on Proof Theory of Concurrent Object-Oriented Programming, July 1996.
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.
D.E. Rydeheard and R.M. Burstall. Computational Category Theory. International Series in Computer Science. Prentice Hall, 1988.
J. Sauloy. A calculus of modules built on a kernel for categorical computations. unpublished.
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.
G. van Rossum. Python tutorial. http://www.python.org/, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michel, P., Wiels, V. (1997). A framework for modular formal specification and verification. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_28
Download citation
DOI: https://doi.org/10.1007/3-540-63533-5_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63533-8
Online ISBN: 978-3-540-69593-6
eBook Packages: Springer Book Archive