Automatic code generation in certified system development: a model-driven specification and verification approach

Arnaud Dieumegard

Institut de Recherche en Informatique de Toulouse
Institut Nationale Polytechnique de Toulouse

Tuesday, 27 November 2012, 11:00 (note the unusal weekday and time)
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: The growing complexity of critical embedded systems significantly impairs their development. The verification requirements from the safety certification rules (e.g DO-178C, ISO-26262) lead to multiple problems that impact specification, development and verification. Common proofreading and/or test-based verification is usually not exhaustive and as systems grow more complex, their coverage is less and less adequate. Use of models allows early verification, validation and automated building of "correct by construction" systems.

Automatic code generation is in use since the early 90ies for tackling the complexity problem. It gives obvious advantages for the development, but verifying its correctness needs still to be addressed. We target the use of common model driven engineering (MDE) techniques to allow ordinary industrial engineers to conduct the specification, verification and validation phases of systems development in a formal manner. From our point of view, automatic code generation is seen as a chain of model transformations that takes as input formal specification of a system's design and generates as output source code. Obviously, these model transformations have to be verified for correctness.

In our work, we target model-based techniques for both specification of user-level elements (e.g Simulink blocks) and verification of model transformations. One of the applications that makes use of this model-based foundation is the transformation of user-specified behavioural properties (contracts) that originate from control theory, from the source model to formal annotations of the output code. Such annotations can then be fed to formal source code analysis tools like Frama-C. We will briefly illustrate such approach with an in progress experiment.

(Joint work with Andres Toom and Marc Pantel.)

Arnaud Dieumegard's visit Tallinn is supported by the ETF/Egide Parrot programme.

Tarmo Uustalu
Last update 27.11.2012