Formal Development Process of Safety-Critical Embedded Human Machine Interface Systems

被引：0

作者：

Ge, Ning ^{[1
,2
,5
]}

Dieumegard, Arnaud ^{[2
]}

Jenn, Eric ^{[2
,6
]}

d'Ausbourg, Bruno ^{[3
]}

Ait-Ameur, Yamine ^{[4
]}

机构：

[1] Beihang Univ, Sch Software, Beijing, Peoples R China

[2] IRT St Exupery, Toulouse, France

[3] Off Natl Etud & Rech Aerosp, Toulouse, France

[4] IRIT ENSEEIHT, Toulouse, France

[5] Systerel, Toulouse, France

[6] Thales Avion, Toulouse, France

来源：

PROCEEDINGS 11TH 2017 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE) | 2017年

关键词：

Human machine interface; formal methods; specification; verification; integration; LIDL; Lustre; HLL; S3; VERIFICATION;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：111 / 118

页数：8

共 50 条

[31] Architectural concepts for embedded systems in safety-critical applications
Skambraks, Martin
Halang, Wolfgang A.
2008 IEEE INTERNATIONAL CONFERENCE ON AUTOMATION, QUALITY AND TESTING, ROBOTICS (AQTR 2008), THETA 16TH EDITION, VOL I, PROCEEDINGS, 2008, : 60 - 65
[32] Quantitative risk analysis of safety-critical embedded systems
Liu, Yinling
Shen, Guohua
Huang, Zhiqiu
Yang, Zhibin
SOFTWARE QUALITY JOURNAL, 2017, 25 (02) : 503 - 527
[33] An Exploratory Study on Applying a Scrum Development Process for Safety-Critical Systems
Wang, Yang
Ramadani, Jasmin
Wagner, Stefan
PRODUCT-FOCUSED SOFTWARE PROCESS IMPROVEMENT (PROFES 2017), 2017, 10611 : 324 - 340
[34] SESAME: A Model-Driven Test Selection Process for Safety-Critical Embedded Systems
Guelfi, Nicolas
Ries, Benoit
ERCIM NEWS, 2008, (75): : 43 - 44
[35] Formal Techniques for Safety-Critical Systems (FTSCS 2016) Preface
Artho, Cyrille
Olveczky, Peter Csaba
SCIENCE OF COMPUTER PROGRAMMING, 2019, 175 : 35 - 36
[36] Formal Techniques for Safety-Critical Systems (FTSCS 2014) Preface
Artho, Cyrille
Olveczky, Peter Csaba
SCIENCE OF COMPUTER PROGRAMMING, 2017, 133 : 89 - 90
[37] Formal Techniques for Safety-Critical Systems (FTSCS 2015) Preface
Artho, Cyrille
Olveczky, Peter Csaba
SCIENCE OF COMPUTER PROGRAMMING, 2018, 154 : 1 - 2
[38] Formal Techniques for Safety-Critical Systems (FTSCS 2018) Preface
Artho, Cyrille
Olveczky, Peter Csaba
SCIENCE OF COMPUTER PROGRAMMING, 2021, 208
[39] HAZOP analysis of formal models of safety-critical interactive systems
Hussey, A
COMPUTER SAFETY, RELIABILITY AND SECURITY, PROCEEDINGS, 2000, 1943 : 371 - 381
[40] Towards a Formal Approach to Analysing Security of Safety-Critical Systems
Vistbakka, Inna
Troubitsyna, Elena
2018 14TH EUROPEAN DEPENDABLE COMPUTING CONFERENCE (EDCC 2018), 2018, : 182 - 189

← 1 2 3 4 5 →