A comprehensive formal specification of ARINC 653 with conformity proof

• Main Authors: FENG, Zhang, ZHAO, Yongwang, YANG, Liu, SUN, Jun
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2024
• Subjects: Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/9499
• Institution: Singapore Management University

As the predominant standard for partitioning operating systems, ARINC 653 has been applied in many critical domains. However, its reliance on informal textual languages presents challenges for ensuring both the correctness of the standard itself and the conformity of a specification or an OS to this standard. This paper addresses the gap through formal work on the ARINC 653 standard. We provide a comprehensive formal specification of multi-core ARINC 653 Part 1–5 using Isabelle/HOL that encompasses all the 68 services and covers all components outlined in the standard, then conduct a formal proof of conformity of the specification according to ARINC 653 Part 3A. Our work marks the first comprehensive multi-core ARINC 653 specification with a formal conformity proof. Notably, we identify and address three defects in the standard document during the formal specification and proof.