Quarteft

with the support of FNRAE

Les objectifs du projet QUARTEFT reposent sur deux constats:

  • la complexité croissante des systèmes embarqués critiques temps-réel conduit à exploiter des langages de modélisation les plus proches possible des spécifications du métier du concepteur. Ces langages s’adossent sur des outils de vérification de modèles permettant d’assurer la correction du système par rapport aux exigences de sûreté, performance, temps-réel, …

  • les chaînes de développement de systèmes critiques basées sur ces langages de modélisation reposent le plus souvent sur des transformations entre langages, comme par exemple la génération automatique de code. Pour augmenter l’assurance que l’on peut placer dans les systèmes ainsi obtenus, ces transformations entre langages doivent être qualifiées (assurance que la transformation préserve les propriétés d’intérêts).

Pour répondre à ces constats, le projet QUARTEFT vise à développer des technologies pour faciliter les activités de modélisation, de transformation et de vérification dans le contexte des systèmes embarqués temps-réel. L’objet du projet QUARTEFT vise à développer les technologies facilitant cette approche en proposant d’une part, une extension temps réel du langage intermédiaire Fiacre, le rapprochant ainsi des langages métiers des systèmes critiques embarqués temps-réel tels que AADL et, d’autre part, de développer les techniques de construction de transformations qui facilitent la preuve de correction et le passage à l’échelle sur des modèles réels. Il s’agit donc de permettre la construction d’une chaîne correcte de transformations des langages utilisateurs vers le langage intermédiaire, puis du langage intermédiaire vers les outils de vérification actuellement disponibles tels que TINA ouCADP. L’expression des transformations et la génération des preuves associées se fera à l’aide de l’outil TOM basé sur des techniques de réécriture. L’ensemble de ces développements sera intégré dans l’outil métier Adele.

Quarteft complète les travaux précédemment réalisés dans le cadre des projets COTRE, TOPCASED, SPICES, GENEAUTO pour assurer la construction de nouvelles générations d’ateliers de développement de systèmes critiques temps-réel basées sur la vérification formelle et les langages dédiés. Les méthodes et outils issus du projet QUARTEFT seront intégrés au sein du processus et de la plate-forme de développement de calculateurs embarqués Airbus (activités produit, électronique et logiciel), issus du projet TOPCASED, de manière à être mis en œuvre opérationnellement sur les futurs programme avion.

Partenaires

  • LAAS-CNRS
    • Bernard Berthomieu Didier Le Botlan Silvano Dal Zilio Pierre-Emmanuel Hladik Francois Vernadat
  • IRIT
    • Jean-Paul Bodeveix Mamoun Filali Marc Pantel Jean-François Rolland
  • ONERA-DTIM
    • David Doose Pierre Michel
  • INRIA Nancy - Grand Est
    • Jean-Christophe Bach Horatiu Cirstea Pierre-Etienne Moreau
  • AIRBUS France
    • Patrick Farail Pierre Gaufillet Marie-Line Valentin
  • Ellidiss
    • Pierre Dissaux Arnaud Schach
Avatar
Silvano DAL ZILIO
CNRS Researcher

My research interests include formal methods and concurrency semantics.

Publications

A formal framework to specify and verify real-time properties on critical systems

We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on …

A Verified Approach for Checking Real-Time Specification Patterns

We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on …

Real-Time Specification Patterns and Tools

An issue limiting the adoption of model checking technologies by the industry is the ability, for non-experts, to express their …

Verification of Real-Time Specification Patterns on Time Transitions Systems

We address the problem of checking properties of Time Transition Systems (TTS), a generalization of Time Petri Nets with data …

Definition of the Fiacre Real-Time Specification Patterns Language

In this report, we define a high-level language for expressing properties over system expressed using Fiacre. Our approach is …

Real-time Extensions for the Fiacre modeling language

We present our ongoing research on the extension of the Fiacre language with real-time constructs and real-time verification …