Temporal and Functional Verification of a Symbolic Representation of Complex Systems

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 formulAE, carrying out automatic proof procedures on these formulAE.