Generation automatique d'une specification formelle a partir de scenarios temps-reels (French text)

A real-time reactive system interacts with its environment under strict timing constraints. The formal specification of such systems is a difficult task that often designers prefer to avoid to move directly from informal specifications to implementation. The detection of design errors and thus the reliability of the system become difficult to evaluate thus increasing the development costs.; This thesis develops automatic methods for synthesis of formal specification in the case of real-time reactive systems. We use a scenario based approach which describes the system behavior by scenarios that are integrated into a global specification. Scenarios describe a system behavior in a particular situation and represent partial specifications of the system. Scenarios based approaches facilitate the task of specification as they use a divide and conquer strategy. Our work focus on development of methods of integration of scenarios which allow automatic synthesis of a formal specification for a real-time reactive system. This formal specification is expressed in the form of a secure timed automaton.; A real-time reactive system conceptualization encompasses static and dynamic aspects. Static aspect deals with system properties with the use of discrete variables, clocks and events. Discrete variables conceptualize the time independent properties of a system. Clocks measure time and are used as time references to enable or disable the execution of an action. Dynamic aspect describes the behavior of the system and uses the static aspect as description language. We call a rule-action the elementary unit of the description of a system behavior. A rule-action states how the state of a system changes after the execution of an action. We define a global semantics of a rule action set by a labeled transition system to which we associate a secure timed automaton. We reduce the combinatorial explosion of the size of this automaton using a bisimulation relation based minimization algorithm.; The description of scenarios is based on a new suite model which hides the formal aspect of the description of a system behavior. However, this scenario model supports the description of a timed constrained behavior. A scenario is a set of execution traces and its semantics is defined by a set of rule-actions which represents the canonical form of this scenario. We thus establish the relation between scenarios and secure timed automata.; Integration of scenarios merges them into a single secure timed automaton. We propose two types of integration methods: implicit integration and explicit integration methods. For each, we define the conformance relation between the initial scenarios and the resulting timed automaton. Implicit integration merge scenarios without any explicit scheduling constraint. Explicit integration uses explicit integration directives which are constraints on the execution order of scenarios. We propose an algorithm to solve the problem of satisfaction of the explicit integration directives. Scenarios which result from this phase, are merged into a timed automaton using implicit integration methods. Furthermore, our approach supports the combination of implicit and explicit integration methods in the same specification. Our scenario based approach supports syntax verification, scenario verification and result of integration verification. We can trace back to the faulty scenario if an error is detected.