Methodology of modeling and verification of critical systems for safe operation

This article presents a method of modeling and verification of the safe operating properties of industrial systems. It represents first of all a data model whose exploitation could be done according to different needs: analysis, evaluation or verification. For system analysis, we propose an object oriented approach for modeling the system and the integration of the necessary data takes into account the aspects of operating safety. This modelling is based on the definition of a UML profile in real time dedicated to this type of analysis. The verification, like the evaluation necessitates recourse to a formal model. Our study concentrates particularly on discrete event systems, we have then chosen Petri networks, considering the multitude of tools existing for simulation and checking.