@inproceedings{360c31c9bc0e4b4d9b61f47541a8eb05,
title = "Formal development process of safety-critical embedded human machine interface systems",
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 software, the development process integrates the following formal activities: modeling the behavioral aspect of user interfaces (UIs) using LIDL; 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 - part of the display component of an alert management system used in a three-wheeled robot.",
keywords = "HLL, Human machine interface, LIDL, Lustre, S3, formal methods, integration, specification, verification",
author = "Ning Ge and Arnaud Dieumegard and Eric Jenn and Bruno D'Ausbourg and Yamine A{\"i}t-Ameur",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017 ; Conference date: 13-09-2017 Through 15-09-2017",
year = "2017",
month = jul,
day = "2",
doi = "10.1109/TASE.2017.8285636",
language = "英语",
series = "Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1--8",
booktitle = "Proceedings - 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017",
address = "美国",
}