Paper Info
Title
Model extraction for ARINC 653 based avionics software
Abstract
One of the most exciting and promising approaches to ensure the correctness of critical systems is software model checking, which considers real code, written with standard programming languages like C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, like spin. This paper presents the application of the technique to avionics software constructed on top of an application interface (API) compliant with the ARINC 653 specification (APEX), which is widely employed by the manufacturers in the avionics industry. The paper uses techniques to automatically extract promela models from C source code. These techniques were previously developed by the authors. However, they are now extended to deal with new problems, like real-time aspects and APEX scheduling. In order to close the extracted model during the verification, we built a reusable APEX-specific environment. This APEX environment models the execution engine (i.e. an APEX compliant RTOS) that implements APEX services. Finally, this paper also contains a novel testing method to ensure the correctness of this APEX environment. This testing method uses SPIN to execute official ARINC 653 test cases.
Year
Venue
Keywords
2007
SPIN
model extraction,software model checking,avionics software,APEX environment,APEX compliant RTOS,promela model,APEX service,reusable APEX-specific environment,APEX environment model,APEX scheduling,reduced model
Field
DocType
Volume
Avionics software,Computer science,Source code,Correctness,Avionics,ARINC 653,Software,Test case,Promela,Embedded system
Conference
4595
ISSN
Citations 
PageRank 
0302-9743
10
0.60
References 
Authors
11
3
Name
Order
Citations
PageRank
Pedro de la Cámara1322.72
María del Mar Gallardo214113.16
Pedro Merino320125.98