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 条

[1] Model-based software development - A Process for safety-critical embedded Systems
Kuschnerus, Dirk
Gerding, Michael
Bilgic, Attila
Musch, Thomas
ATP EDITION, 2012, (7-8): : 60 - 66
[2] FORMAL VERIFICATION OF SAFETY-CRITICAL SYSTEMS
MOSER, LE
MELLIARSMITH, PM
SOFTWARE-PRACTICE & EXPERIENCE, 1990, 20 (08): : 799 - 821
[3] FORMAL METHODS FOR SAFETY-CRITICAL SYSTEMS
MCARTHUR, N
CONTROL AND INSTRUMENTATION, 1994, 26 (05): : 59 - 60
[4] On the formal development of safety-critical software
Galloway, Andy
Iwu, Frantz
McDermid, John
Toyn, Ian
VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 362 - 373
[5] FORMAL METHODS - USE AND RELEVANCE FOR THE DEVELOPMENT OF SAFETY-CRITICAL SYSTEMS
BARROCA, LM
MCDERMID, JA
COMPUTER JOURNAL, 1992, 35 (06): : 579 - 599
[6] Human performance and embedded intelligent technology in safety-critical systems
Grabowski, M
Sanborn, SD
INTERNATIONAL JOURNAL OF HUMAN-COMPUTER STUDIES, 2003, 58 (06) : 637 - 670
[7] Formal verification of safety-critical hybrid systems
Livadas, C
Lynch, NA
HYBRID SYSTEMS: COMPUTATION AND CONTROL, 1998, 1386 : 253 - 272
[8] THE PRACTICE OF FORMAL METHODS IN SAFETY-CRITICAL SYSTEMS
LIU, SY
STAVRIDOU, V
DUTERTRE, B
JOURNAL OF SYSTEMS AND SOFTWARE, 1995, 28 (01) : 77 - 87
[9] Formal Techniques for Safety-Critical Systems Preface
Artho, Cyrille
Olveczky, Peter Csaba
SCIENCE OF COMPUTER PROGRAMMING, 2015, 113 : 83 - 84
[10] Formal Verification of Safety-Critical Aerospace Systems
Paul, Saswata
Cruz, Elkin
Dutta, Airin
Bhaumik, Ankita
Blasch, Erik
Agha, Gul
Patterson, Stacy
Kopsaftopoulos, Fotis
Varela, Carlos
IEEE AEROSPACE AND ELECTRONIC SYSTEMS MAGAZINE, 2023, 38 (05) : 72 - 88

← 1 2 3 4 5 →