Ge, Ning and Dieumegard, Arnaud and Jenn, Eric and D'Ausbourg, Bruno and Aït-Ameur, Yamine
Formal development process of safety critical embedded human machine interface systems.
(2018)
In: TASE (11th International Symposium on Theoretical Aspects of Software Engineering), 13 September 2017 - 15 September 2017, Sophia Antipolis (France) (Sophia Antipolis, France).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 603kB |
Official URL: http://dx.doi.org/10.1109/TASE.2017.8285636
Abstract
This paper presents a formal development process for safety-critical embedded Human-Machine Interface (HMI) systems. This formal approach is centered on the LIDL formal language and the S3 verification toolset. It is aimed at blurring the boundaries between modeling, design, verification and implementation for the development of HMI. From textual requirements to safety-critical embedded software, the development process integrates the following formal activities: modeling the behavioral aspect of user interfaces (UIs) using the LIDL language; translating LIDL to Lustre, with which we combine the functional library in Lustre; translating the Lustre design models into the HLL verification models; verifying formal properties expressed in HLL against the HLL model using the S3 toolset, and diagnosing design errors with the help of counterexample scenarios and debug tools. This formal development process is illustrated on a simple use case of part of the display component of an alert management system embedded in a three-wheeled robot.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to IEEE. The original document is available on IEEE Xplore : http://ieeexplore.ieee.org/document/8285636/ © 2017 . Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. |
| HAL Id: | hal-01740640 |
| Audience (conference): | International conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE) Other partners > Thales (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) Other partners > Beihang University (CHINA) Other partners > IRT Saint Exupéry - Institut de Recherche Technologique (FRANCE) Other partners > SYSTEREL (FRANCE) |
| Laboratory name: | |
| Funders: | INGEQUIP project |
| Statistics: | download |
| Deposited On: | 22 Mar 2018 10:09 |
Repository Staff Only: item control page
