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 条
  • [41] Safety certification of airborne software: An empirical study
    Dodd, Ian
    Habli, Ibrahim
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 2012, 98 (01) : 7 - 23
  • [42] LEGAL IMPLICATIONS OF SAFETY CERTIFICATION FOR SOFTWARE PRODUCTS
    LLOYD, IJ
    SIMPSON, MJ
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 1994, 43 (02) : 169 - 175
  • [43] Software Certification: Is There a Case against Safety Cases?
    Wassyng, Alan
    Maibaum, Tom
    Lawford, Mark
    Bherer, Hans
    FOUNDATIONS OF COMPUTER SOFTWARE: MODELING, DEVELOPMENT, AND VERIFICATION OF ADAPTIVE SYSTEMS, 2011, 6662 : 206 - 227
  • [44] Experience Report: Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework
    Pagano, Bruno
    Andrieu, Olivier
    Moniot, Thomas
    Canou, Benjamin
    Chailloux, Emmanuel
    Wang, Philippe
    Manoury, Pascal
    ICFP'09: PROCEEDINGS OF THE 2009 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2009, : 215 - 219
  • [45] Experience Report: Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework
    Pagano, Bruno
    Andrieu, Olivier
    Moniot, Thomas
    Canou, Benjamin
    Chailloux, Emmanuel
    Wang, Philippe
    Manoury, Pascal
    Colaco, Jean-Louis
    ACM SIGPLAN NOTICES, 2009, 44 (8-9) : 215 - 219
  • [46] A STRATEGY FOR IDENTIFICATION AND DEVELOPMENT OF SAFETY CRITICAL SOFTWARE EMBEDDED IN COMPLEX-SPACE SYSTEMS
    WUNRAM, J
    ACTA ASTRONAUTICA, 1993, 29 (03) : 213 - 221
  • [47] 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
  • [48] A Bridge from System to Software Development for Safety-Critical Automotive Embedded Systems
    Mader, Roland
    Griessnig, Gerhard
    Armengaud, Eric
    Leitner, Andrea
    Kreiner, Christian
    Bourrouilh, Quentin
    Steger, Christian
    Weiss, Reinhold
    2012 38TH EUROMICRO CONFERENCE ON SOFTWARE ENGINEERING AND ADVANCED APPLICATIONS (SEAA), 2012, : 75 - 79
  • [49] Hardware software codesign of a safety-critical embedded computer system for an automatic endoscope
    Khan, GN
    Jin, M
    IEEE CCEC 2002: CANADIAN CONFERENCE ON ELECTRCIAL AND COMPUTER ENGINEERING, VOLS 1-3, CONFERENCE PROCEEDINGS, 2002, : 657 - 662
  • [50] The Right Degree of Configurability for Safety-Critical Embedded Software in Variable Message Signs
    Novak, Thomas
    Stoegerer, Christoph
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, 2010, 6351 : 418 - 430
12345