Abstract
The complexity of systems requires that validation methods are set in the designing phase as well as during their use or maintenance. We propose a modelling approach of the system which allows us to bring into play some methods for the validation of temporal and functional properties. The model that we have defined, called Interpreted Sequential Machine, is based on the concept of Sequential Machine and avoids the main limitation (combinatorial explosion of the number of states when introducing any new data) by separating the purely sequential part of the system from the data and the operations on the data. The validation of the complex system thus modelled consists in:
-
expressing the behaviour of the system by a set of symbolic, logicotemporal formulÆ,
-
carrying out automatic proof procedures on these formulÆ.
Preview
Unable to display preview. Download preview PDF.
References
Audureau, E., Enjalbert, P., Farinas del Cerro, L.: Logique Temporelle — Sémantique et validation de programmes parallèles. Masson, Paris (1990)
Chang, K.T., Krishnakumar, A.S.: Automatic functional test generation using the Extended Finite State Machine Model. 30th ACM/IEEE Design Automation Conference, USA (1993)
Kohavi, Z.: Switching and Finite Automata Theory. Tata McGraw Hill, Computer Science Series (1978)
Magnier, J.: Represéntation symbolique et vérification formelle de machines séquentielles. PhD Thesis, University of Montpellier II, France (July 1990)
Magnier, J., Pearson, D., Giambiasi, N.: The Temporal Boolean Derivative Applied to Verification of Sequential Machines. European Simulation Symposium, Istanbul, Turkey (1994)
Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. Report No STAN-CS-82-954, Department of Computer Science, Stanford University (1982)
Vandermeulen, E., Donegan, H.A., Larnac, M., Magnier, J.: The Temporal Boolean Derivative Applied to Verification of Extended Finite State Machines. Computers and Mathematics with Applications, Vol.30, N. 2 (January 1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larnac, M., Magnier, J., Vandermeulen, E., Dray, G., Chapurlat, V. (1996). Temporal and functional verification of a symbolic representation of complex systems. In: Pichler, F., Díaz, R.M., Albrecht, R. (eds) Computer Aided Systems Theory — EUROCAST '95. EUROCAST 1995. Lecture Notes in Computer Science, vol 1030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0034757
Download citation
DOI: https://doi.org/10.1007/BFb0034757
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60748-9
Online ISBN: 978-3-540-49358-7
eBook Packages: Springer Book Archive