Title :
SAFEBOX: A Verified Microkernel Based on Spatial-Temporal Isolation
Author :
Fan Zhang ; Weining Su ; Tianfang Wang ; Xiaopeng Wang
Author_Institution :
Sch. of Comput. Sci., Northwestern Polytech. Univ., Xi´an, China
Abstract :
The correctness of kernel is the key to the safety-critical embedded application, and only by formal verification it can prove the kernel does not exist some defects or meet certain attributes. In this paper, we introduce SAFEBOX, a microkernel based on spatial-temporal isolation, give the formal description of SAFEBOX, and use theorem proverb Isabelle/HOL to verify the functional and non-functional properties of SAFEBOX.
Keywords :
formal verification; safety-critical software; theorem proving; HOL; SAFEBOX; formal description; formal verification; functional properties; nonfunctional properties; safety-critical embedded application; spatial-temporal isolation; theorem prover Isabelle; verified microkernel; Arrays; Embedded software; Embedded systems; Formal verification; Instruction sets; Kernel; Schedules; Formal verification; Microkernel; Safety-Critical; Temporal-Spatial Isolation;
Conference_Titel :
Information Science and Control Engineering (ICISCE), 2015 2nd International Conference on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4673-6849-0
DOI :
10.1109/ICISCE.2015.105
