A formal approach for the specification and the verification of real-time systems
Une approche formelle pour la spécification et la vérification des systèmes temps-réel
Résumé
Our aim is the use of formal techniques for the development of control-command system, which constitutes the program component of real-time systems. Generally, using a formal method for program development first consists in formally specifying the expected behaviour of the target program and then in proving that the program implementation satisfies this specification. We can adopt this strategy in real-time systems and develop the control-command program by means of specifying its behaviour. Nevertheless, it seems more natural to proceed otherwise. In fact, a real-time system or an automated system is constituted by one" imposed" operative part, which acts on its environment, and a control program (automation system) piloting the physical system. The system, whose behaviour interests the user, is the automated one and not the automation one, which is the task of the developer. The automated system aots on an environment which itself may be assumed as a system i.e. the target system. It is defined by abstraction. The user objective is then to have an automated system satisfying target system requirements. However, the challenge for the developer is to design a suitable development methodology for this end. In a first part of this thesis, we propose a development methodology for the specification and the verification of automation system, given the automated system and operative part descriptions. We exhibit different behaviour properties of these systems, which needs the prediction of system's behaviour in the future, given the observed behaviour ending at a certain point. In this context, we extend temporal logic with new operators and propose a new language called IPTL for reasoning about such properties, defining the relationship between system behaviour in the future and its history. We illustrate our approach through industrial examples and prove that the specification and verification processes.
Notre but est d'utiliser des techniques formelles pour le développement de systèmes d'automatisation (système de contrôle-commande) formant le composant logiciel d'un système temps-réel. Succinctement, utiliser une méthode formelle pour le développement d'un logiciel consiste à spécifier de façon formelle le comportement attendu du logiciel sous forme de propriétés, et à prouver que le logiciel lui-même satisfait cette spécification. Une spécification exprime les besoins de l'utilisateur et sert aussi de référence au développeur. Dans le cas des applications temps-réel, le système dont le comportement intéresse l'utilisateur est le système automatisé formé d'une partie physique qui existe et d'un système d'automatisation qu'on cherche à développer. L'utilisateur souhaite que le système automatisé agisse sur un environnement (système cible) de façon que ce dernier se comporte selon ses souhaits. Étant donné qu'un système temps-réel contient des composants physiques préexistants, il nous est apparu que son développement doit se faire de façon différente que pour les logiciels classiques. Dans ce mémoire, nous proposons d'abord une méthodologie de développement qui consiste à construire et valider une spécification formelle du système d'automatisation, compte tenu de la description du système automatisé et de la partie opérationnelle. Nous montrons que le cadre méthodologique s'adapte à différents cas de systèmes temps-réel. Nous examinions ensuite nos besoins de spécification pour les différents composants d'un système temps-réel qui nécessitent de pouvoir exprimer l'évolution prévisible en fonction d'un comportement observé jusqu'à un certain point. Ceci nous amène à compléter les opérateurs de la logique temporelle classique par de nouveaux opérateurs et à proposer un nouveau langage de spécification dénommé LTPI, conçu comme une extension de la logique temporelle, et qui permet de décrire une partie du comportement d'un système comme une conséquence d'une autre partie qui l'a précédée. Nous illustrons notre approche à travers quelques exemples de cas industriels, et nous prouvons que le processus de spécification et de vérification se simplifie en utilisant le formalisme proposé.