Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B

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.