Applying formal proof techniques to avionics software: A pragmatic approach

被引：0
|
作者：
Randimbivololona, F
Souyris, J
Baudin, P
Pacalet, A
Raguideau, J
Schoen, D
机构：
[1] Aerosp Matra Airbus, F-31060 Toulouse, France
[2] CEA Saclay, LETI, DEIN, F-91191 Gif Sur Yvette, France
来源：
FM'99-FORMAL METHODS, VOL II | 1999年 / 1709卷
关键词：
D O I：
暂无
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
This paper reports an industrial experiment of formal proof techniques applied to avionics software. This application became possible by using Caveat, a tool dedicated to assistance in comprehension and formal verification of safety critical applications written in C. With this approach it is possible to reduce significantly the actual verification effort (based on test) in achieving the verification objectives defined by the DO 178B [4].
引用
收藏
页码：1798 / 1815
页数：18
相关论文
共 50 条
  • [41] A formal approach to distributed software architecture
    He, J
    Fang, DY
    Qin, Z
    2002 IEEE REGION 10 CONFERENCE ON COMPUTERS, COMMUNICATIONS, CONTROL AND POWER ENGINEERING, VOLS I-III, PROCEEDINGS, 2002, : 342 - 346
  • [42] A formal approach to designing anonymous software
    Kawabe, Yoshinobu
    Sakurada, Hideki
    SERA 2007: 5TH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH, MANAGEMENT, AND APPLICATIONS, PROCEEDINGS, 2007, : 203 - +
  • [43] A formal approach to heterogeneous software modeling
    Egyed, A
    Medvidovic, N
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2000, 1783 : 178 - 192
  • [44] Applying and optimizing Trajectory approach for performance evaluation of AFDX avionics network
    Bauer, Henri
    Scharbarg, Jean-Luc
    Fraboul, Christian
    2009 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION (EFTA 2009), 2009,
  • [45] Formal firewall conformance testing: an application of test and proof techniques
    Brucker, Achim D.
    Bruegger, Lukas
    Wolff, Burkhart
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2015, 25 (01): : 34 - 71
  • [46] On applying formal techniques to the development of hybrid services: Challenges and directions
    Logean, X
    Dietrich, F
    Hubaux, JP
    Grisouard, S
    Etique, PA
    IEEE COMMUNICATIONS MAGAZINE, 1999, 37 (07) : 132 - 138
  • [47] ON USING FORMAL SOFTWARE ENGINEERING TECHNIQUES IN AN ACADEMIC ENVIRONMENT
    ANSON, CP
    HARRISON, RL
    LEWELLEN, TK
    GILLISPIE, SB
    POLLARD, KP
    BICE, AN
    MIYAOKA, RS
    HAYNOR, DH
    ZHU, J
    IMAGES OF THE TWENTY-FIRST CENTURY, PTS 1-6, 1989, 11 : 2011 - 2012
  • [48] Applying Formal Verification Techniques to Ambient Assisted Living Systems
    Benghazi, Kawtar
    Visitacion Hurtado, Maria
    Luisa Rodriguez, Maria
    Noguera, Manuel
    ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS: OTM 2009 WORKSHOPS, 2009, 5872 : 381 - 390
  • [49] A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs
    Tuan Minh Pham
    Bertot, Yves
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 285 : 43 - 55
  • [50] Formal Techniques for Hardware/Software Co-Verification
    Kroening, Daniel
    Srivas, Mandayam
    2013 26TH INTERNATIONAL CONFERENCE ON VLSI DESIGN AND 2013 12TH INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS (VLSID), 2013, : LVII - LVIII
12345