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 条
12345