Title
Abstract specification and formalization of an operating system kernel in Z
Abstract
One of the mini challenges in software verification related to the Grand Challenge proposed by Tony Hoare concerns the formal specification and verification of an operating system kernel. This paper proposes a simple and correct specification of an OS kernel in Z which simplifies the understanding and verification of operating system components. Our current specification comprises process management, interprocess communication and a POSIX-compliant file system.
Year
DOI
Venue
2011
10.1145/1945023.1945042
Operating Systems Review
Keywords
DocType
Volume
os kernel,current specification,posix-compliant file system,abstract specification,correct specification,formal specification,software verification,operating system kernel,grand challenge,tony hoare,system component,operating system,interprocess communication,process management
Journal
45
Issue
Citations 
PageRank 
1
0
0.34
References 
Authors
8
5
Name
Order
Citations
PageRank
Luciano Barreto1253.58
Aline Andrade2143.47
Adolfo Duran3103.30
Caique Lima400.34
Ademilson Lima500.34