A Formal Specification of Operating System based on ARINC 653
Ziyan Wang, Yan Zhang
TL;DR
This paper presents a formal specification of an ARINC 653-based operating system using Circus, covering core functionalities like interrupt handling, scheduling, and concurrent behaviors of partitions and processes.
Contribution
It introduces a comprehensive formal model of an ARINC 653 OS, including concurrency, interrupt handling, and system services, using the Circus language.
Findings
Formal specification of core OS components
Modeling of concurrent behaviors of partitions and processes
Enhanced understanding of ARINC 653 OS design
Abstract
In this paper, by using the formal language \emph{Circus}, we give a formal specification of an operating system based on ARINC 653 standard. Our specification includes interrupt handling, time and memory management, partition and process scheduling, system call response and related APEX services. Especially, the concurrent behaviours of partitions and processes are also specified.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsReal-Time Systems Scheduling · Embedded Systems Design Techniques · Distributed and Parallel Computing Systems