Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B
This work addresses safety and certification issues for developers of safety-critical real-time operating systems and applications, though it is incremental as it applies an existing formal method to a specific standard.
The authors tackled the problem of errors in safety-critical system standards by formalizing and verifying the ARINC 653 standard using Event-B, discovering six hidden errors in the process.
Standards play the key role in safety-critical systems. Errors in standards could mislead system developer's understanding and introduce bugs into system implementations. In this paper, we present an Event-B formalization and verification for the ARINC 653 standard, which provides a standardized interface between safety-critical real-time operating systems and application software, as well as a set of functionalities aimed to improve the safety and certification process of such safety-critical systems. The formalization is a complete model of ARINC 653, and provides a necessary foundation for the formal development and verification of ARINC 653 compliant operating systems and applications. Six hidden errors were discovered from the verification using the Event-B formal reasoning approach.