A comprehensive formal specification of ARINC 653 with conformity proof

Publication Type

Journal Article

Publication Date

10-2024

Abstract

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.

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Software: Testing, Verification and Reliability

First Page

1

Last Page

17

ISSN

0960-0833

Identifier

10.1002/stvr.1901

Publisher

Wiley

Additional URL

https://doi.org/10.1002/stvr.1901

This document is currently not available here.

Share

COinS