Verification of real time properties in fiacre language

The formal verification of critical, reactive systems is a very complicated task, especially for non experts. In this work, we more particularly address the problem of real time systems, that is in the situation where the correctness of the system depends upon timing constraints, such as the "timeliness" of some interactions. Many solutions have been proposed to ease the specification and the verification of such systems. An interesting approach--that we follow in this thesis--is based on the definition of specification patterns, that is sets of general, reusable templates for commonly occurring classes of properties. However, patterns are rarely implemented, in the sense that the designers of specification languages rarely provide an effective verification method for checking a pattern on a system. The most common technique is to rely on a timed extension of a temporal logic to define the semantics of patterns and then to use a model-checker for this logic. However, this approach may be inadequate, in particular if patterns require the use of a logic associated to an undecidable model-checking problem or to an algorithm with a very high practical complexity. We make several contributions. We propose a complete theoretical framework to specify and check real time properties on the formal model of a system. First, our framework provides a set of real time specification patterns (that may be viewed as a timed extension of Dwyer's patterns). We provide a verification technique based on the use of observers that has been implemented in a tool for the Fiacre modelling language. Finally, we provide two methods to check the correctness of our verification approach; a "semantics"-theoretical-method as well as a "graphical"-practical- method.Pas de résumés en françai