Paper Info
Title
Verification of Real Time Operating System Exception Management Based on SPARCv8
Abstract
Exception management, as the lowest level function module of the operating system, is responsible for making abrupt changes in the control ow to react to exception events in the system. The correctness of the exception management is crucial to guaranteeing the safety of the whole system. However, existing formal verification projects have not fully considered the issues of exceptions at the assembly level. Especially for real-time operating systems, in addition to basic exception handling, there are nested exceptions and task switching by exceptions service routine. In our previous work, we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer. Building on earlier work, this paper proposes EMS (Exception Management SPARCv8), a practical Hoare-style program framework to verify the exception management based on SPARCv8 (Scalable Processor Architecture Version 8) at the design layer. The framework describes the low-level details of the machine, such as registers and memory stack. It divides the execution logic of the exception management into six phases for comprehensive formal modeling. Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example, we use the EMS framework to verify the exception management. All the formalization and proofs are implemented in the interactive theorem prover Coq.
Year
DOI
Venue
2021
10.1007/s11390-021-1644-x
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY
Keywords
DocType
Volume
operating system, exception, Scalable Processor Architecture Version 8 (SPARCv8), Coq, formal verification
Journal
36
Issue
ISSN
Citations 
6
1000-9000
0
PageRank 
References 
Authors
0.34
0
5
Name
Order
Citations
PageRank
Zhi Ma100.34
Lei Qiao225.43
Mengfei Yang300.34
Shao-Feng Li400.34
Jin-Kun Zhang500.34