THE ISM: A FORMAL TOOL FOR MODELLING AND VERIFICATION

Abstract

This paper addresses the issue of modelling and analysis of systems. The necessity of carrying out verification and/or validation tasks is discussed, the factors which influence the choice of a model are shown, and the differences between simulation tools or formal methods is explained. Within the framework of discrete time modelling of systems, a method for formally analysing the behaviour of a system described by a Finite State Machine permits to prove properties: the method is based on the translation into a formal system which has got a temporal logic interpretation, and the analysis of the sensitivity of the temporal evolution of the system with respect to some events involves the use of the Temporal Boolean Difference. Furthermore, in order to improve the expressiveness power of the model, an extension of the Finite State Machine model, called Interpreted Sequential Machine (lSM) supports the representation of complex data. The verification process has been adapted to t his model.