Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B
Abstract
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.
Cite
@article{arxiv.1508.06479,
title = {Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B},
author = {Yongwang Zhao and Zhibin Yang and David Sanan and Yang Liu},
journal= {arXiv preprint arXiv:1508.06479},
year = {2015}
}
Comments
12 pages