Une approche formelle pour la spécification et la vérification des systèmes temps-réel

Abstract : 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.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/INPL_T_2000_JEMNI_BEN_AYED_L.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01750490
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:47:34 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:21 PM

Identifiers

  • HAL Id : tel-01750490, version 1

Collections

Citation

Leila Jemni Ben Ayed. Une approche formelle pour la spécification et la vérification des systèmes temps-réel. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2000. Français. ⟨NNT : 2000INPL023N⟩. ⟨tel-01750490⟩

Share

Metrics

Record views

38