Combination of static and dynamic analyses for the certification of avionics software

被引：3

作者：

Ferlin, Antoine ^{[1
]}

Wiels, Virginie ^{[2
]}

机构：

[1] Airbus Operat SAS, ONERA, EYYWDV, DTIM, Toulouse, France

[2] Off Natl Etud & Rech Aerosp, DTIM, Toulouse, France

来源：

23RD IEEE INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING WORKSHOPS (ISSRE 2012) | 2012年

关键词：

avionics; software verification; LTL; dynamic analysis; VERIFICATION;

D O I：

10.1109/ISSREW.2012.100

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper proposes a dynamic analysis approach developed for the verification of avionics software. The objective is to formally verify temporal properties on execution traces. The approach consists of three steps: computation of the necessary observation points in the program using static analysis, execution of the program and generation of the execution trace, verification of the temporal property on the trace. The approach has been implemented in a tool.

引用

页码：331 / 336

页数：6