Sciweavers

Share
SPIN
2007
Springer

Model Extraction for ARINC 653 Based Avionics Software

9 years 3 months ago
Model Extraction for ARINC 653 Based Avionics Software
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 modelling techniques previously developed by the authors. However, these techniques are now extended to deal with new problems, like real-time aspects and scheduling. The paper also contains a novel testing method to ensure the correctness of the key part in the model: the execution engine that implements apex services. This testing method uses spin to execute official test ...
Pedro de la Cámara, María-del-Mar Ga
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SPIN
Authors Pedro de la Cámara, María-del-Mar Gallardo, Pedro Merino
Comments (0)
books