Extended temporal proof of properties using the interpreted sequential machine model

Verification and validation appear to be crucial tasks within each phase of a system life-cycle. The impact of an undetected specification or design error within a project can appear to be of tremendous importance. The possibilities to perform verification or validation are either to make, when possible, a prototype of the real system and evaluate its appropriateness, or to build a model of the system and to analyze it. The most current approach is then to run some simulation; a complementary one is to handle formal reasoning without any execution. The paper develops a process for formal proof of properties of discrete state models. The main stress concerns the temporal evolution of the modeled systems. The method consists in representing the behavior of the system thanks to a state model, to translate it into a temporal logic framework and then to evaluate the existence of properties expressed as formulae. The first application is made on the classical FSM. It is then extended to the interpreted sequential machine, which is a state model able to consider any type of data. Moreover, using some graph theory results, it was possible to widen the proof of properties to the concept of “generic future”