Proposal of a logical formalism for the expression and the verification of temporal properties on repetitive events aimed at execution trace analysis

To provide safety analysis of complex real time systems which have been developed for the protection of French nuclear Plants, the French research center of nuclear area namely the Commissariat a l'Energie Atomique (CEA) is interested in software testing validation techniques. These series of tests are made by a purely software simulation of the system. The purpose is to establish the truth of some critical properties of the program either at the simulation run time or after its execution. The operator is able to describe the variation of some inputs parameters of the program and shows the results with graphics facilities. An important need was to describe formally some categories of properties expressed in terms of academic examples. We thought that a logical textual language was appropriate to achieve this formal expression. This thesis describes a new Data flow language called EFRI extending the semantic of interval temporal logics. Then we describe a calculus using regular languages on arrays which associates to each formula of the EFRI language can be viewed as a classical problem of languages theory: does a word belongs to a regular language? We can then build a finite automata to recognize complex temporal diagrams. (author)