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 ...

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: Pedro de la Cámara, María-del-Mar Gallardo, Pedro Merino
• Keywords: Arinc 653 Specification, Method Uses Spin, SPIN 2007, Testing Method, Theoretical Computer Science