Nos partenaires

CNRS

Rechercher





Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe ACADIE > Recherches

Development of Critical Software

We address the development of critical software through semantic models : Timed models, structuring design concepts : contract-based design and languages : Real-time languages. More generally, we address the integration of formal methods and model driven engineering.

Timed models

This work has started five years ago and lead to two PhD theses. Its main objective was to formally reason on timed system modeling languages, and their properties. Two main notions have been considered : composition and simulation. Concerning composition, we have proposed a variant of the semantics of timed automata with UPPAAL committed location so that their product becomes compositional. More precisely, the Time Transition Systems (TTS)-based semantics of the product of timed automata is the TTS product of the semantics of individual timed automata. This property together with simulation allows the compositional development and verification of timed automata-based systems. Furthermore, model checking remains possible through a transformation to timed automata with UPPAAL semantics. Concerning timed simulation, several specialized tools exist and compare variants of timed automata-based systems with numerous restrictions. We have proposed a criterion that can be expressed using untimed modal mu-calculus and proved its completeness and correctness for a given class of timed transition systems. Restrictions are still needed but no specific tool is necessary : experiments have been done using the FIACRE/TINA toolchain. Lastly, the models and their properties have been specified using the proof assistant Coq. All the obtained results have been proved in Coq using an axiomatization of the time domain which allows discrete or continuous time models.

Contract based design

In the software engineering literature, the term contract refers to the set of specifications that describe what a system should guarantee under some assumptions about its context of use. Nowadays, manufacturers perform system design and integration by importing/reusing entire subsystems provided by equipment suppliers. By promoting a contract-based design approach, design in isolation can be assessed and component integration and substitution can be eased. During the period, we have shown that a logical formalism based on modalities is particularly suitable for contract specification. We have developed a full contract algebra composed of a notion of structural refinement, which allows for automatic abstraction and refinement of models and guides their implementation. It also comes equipped with logical operations such as conjunction, permitting the logical combination of several contracts of the same component into one, and with structural operations such as composition, which formally models composability and composition of contracts, and quotient, permitting automatic synthesis of missing component contracts. Next, in order to cope with real time systems, a timed extension of modal contracts and its algebra has been developed. Beyond modular design, we have shown that contracts can also be used in two different contexts : logical causality (by opposition to the traditional temporal causality) in which contracts are exploited to establish liabilities in case of system failures ; separate compilation of synchronous programs.

Real-time languages

Embedded systems have often a real-time nature. In the context of the avionics domain, we have considered the AADL language since it is a standard. We have especially studied the semantics of so called synchronous subsets of the AADL execution model and how to verify AADL designs using model-checking based verification tool chains. With respect to semantics, we have mainly considered the synchronous approach and studied various semantic models and their relations. The motivation of theses studies were the following : correctness and soundness of the clock constraints synthesis, investigation of models well suited for code generation targeting multicore platforms. Last, we have also been interested in formalizing and validating the usual components of real-time platforms like schedulers. All these studies have been undertaken with a theorem proving approach (Coq, Isabelle). It is interesting to remark that the studies undertaken here are a witness of the common and shared interests of all the groups of the team. Actually, we have to model infinite computations which require advanced concepts of type theory. Moreover, since these computations are distributed and real-time, the proof of their properties require to understand the mechanisms of the underlying domain in order to model them faithfully and structure them carefully. Thanks to this broad approach, the team has played a major role in projects where the design of architecture-based languages where the concern.

Integration of Formal Methods and Model Driven Engineering

These activities take place in the domain of formal method and language engineering. They target methods and tools to ease the integration of FM and MDE in the development of safety critical systems. During this period, they focused on three key aspects : a) the specification of domain specific modeling language (DSML) semantics and its application to tool building, b) the design of property driven verification tools, c) the specification and verification of model transformations. Their results should be used by the usual software engineers from industrial partners for the implementation of tools taking into account safety critical system development standards. Thus, they rely on standard technologies from MDE on the specification side like MOF, OCL, CVL, action languages, transformation models, ... that are mapped to formal technologies used in the academia for validation and verification purpose. More precisely, a common formal specification is used both by the industrial partners to build tools assessed at each use in a translation validation manner ; and by academic partners to prove once the correctness of the toolset. This has been applied to prove the correctness of Simulinkx model transformations. One major part of the specification formalizes the DSMLs involved in the tools. This formalization is then used to prove the correctness of the specification and to generate proof objective at each transformation use. It has also been applied to Simulink models. Instead of using generic transformations from user to verification models targeting many kinds of properties that usually lead to scalability issues at verification time, a property driven method has been proposed for the design of model verification tools. It relies on user level specification of model verification requirements that allow deriving specific transformations from user to verification models and from verification results to model diagnostic. Tools have been designed to automate partly the methodology. This method has been validated on the SPEM, Ladder and BPEL languages for domain specific properties using the FIACRE language as intermediate. A more complex experiment has been conducted for UML models (composite structure, state machine and activity diagrams) focusing on qualitative and quantitative real time properties. Each step (behavior and requirement translation, observer implementation, model reduction, feedback analysis) has been specialized to scale as best as possible for specific kind of properties. A collaboration with the INRIA PAREO team was conducted to extend the TOM toolset to implement model transformations that build transformation model instances during each application of the transformation. These instances then provide the required traceability data for certification and transformation validation. In cooperation with INRIA Triskell team, a shallow embedding of MOF in the Coq proof assistant was designed. It has been actually used to prove the correctness of MDE tools.