A provably correct embedded verifier for the certification of safety critical software

被引：0
|
作者：
Cimatti, A [1 ]
Giunchiglia, F
Pecchiari, P
Pietra, B
Profeta, J
Romano, D
Traverso, F
Yu, B
机构：
[1] IRST, Sci & Technol Res Inst, I-38050 Trento, Italy
[2] Ansaldo Trasporti Spa, I-16100 Genoa, Italy
[3] Ansaldo Signal, Pittsburgh, PA 15219 USA
来源：
COMPUTER AIDED VERIFICATION | 1997年 / 1254卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
VFRAME is one of ANSALDO'S software driven vital architectures for safety critical products. This paper describes a project whose result is the development of an "embedded verifier", i.e. a system integrated within VFRAME and able to certify the correctness of one of VFRAME components, a compiler. The embedded verifier satisfies two precise requirements. First, the compiler must be certified in a fully automatic and efficient way. Second, the embedded verifier must be itself certified, in a way which can be easily understood and validated by end users.
引用
收藏
页码：202 / 213
页数：12
相关论文
共 50 条
  • [21] A Controlled Experiment in Testing of Safety-Critical Embedded Software
    Enoiu, Eduard P.
    Causevic, Adnan
    Sundmark, Daniel
    Pettersson, Paul
    2016 9TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), 2016, : 1 - 11
  • [22] Testing of Safety-Critical Software Embedded in an Artificial Heart
    Cha, Sungdeok
    Jeong, Sehun
    Yoo, Junbeom
    Kim, Young-Gab
    ADVANCES IN SYSTEMS SAFETY, 2011, : 143 - +
  • [23] Validation and certification of safety-critical embedded systems -: The DECOS test bench
    Schoitsch, Erwin
    Althammer, Egbert
    Eriksson, Henrik
    Vinter, Jormy
    Goenczy, Laszlo
    Pataricza, Andras
    Csertan, Gyoergy
    COMPUTER SAFETY, RELIABILTIY, AND SECURITY, PROCEEDINGS, 2006, 4166 : 372 - 385
  • [24] UML for Software Safety and Certification Model-Based Development of Safety-Critical Software-Intensive Systems
    Huhn, Michaela
    Hungar, Hardi
    MODEL-BASED ENGINEERING OF EMBEDDED REAL-TIME SYSTEMS, 2010, 6100 : 201 - +
  • [25] Software and hardware certification of safety-critical avionic systems: A comparison study
    Youn, Wonkeun
    Yi, Baeck-jun
    COMPUTER STANDARDS & INTERFACES, 2014, 36 (06) : 889 - 898
  • [26] Quality assurance and software certification in respect to software construction of safety critical X-by-wire systems
    Kühl, M
    Müller-Glaser, KD
    ELECTRONIC SYSTEMS FOR VEHICLES, 2003, 1789 : 467 - 475
  • [27] Quality assurance and software certification in respect to software construction of safety critical X-by-wire systems
    Kühl, Markus
    Müller-Glaser, K.D.
    VDI Berichte, 2003, (1789): : 3519 - 3527
  • [28] A Provably Correct MPC Approach to Safety Control of Urban Traffic Networks
    Sadraddini, Sadra
    Belta, Calin
    2016 AMERICAN CONTROL CONFERENCE (ACC), 2016, : 1679 - 1684
  • [29] Analysis of Errors in Safety Critical Embedded System Software in Aerial Vehicle
    Lakshmi, K. V. N. S.
    Kumar, Sanjeev
    INFORMATION, COMMUNICATION AND COMPUTING TECHNOLOGY, 2017, 750 : 246 - 257
  • [30] Model-Driven Engineering and Safety-Critical Embedded Software
    Shukla, Sandeep K.
    COMPUTER, 2009, 42 (09) : 93 - 95
12345