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 Barreto | 1 | 25 | 3.58 |
Aline Andrade | 2 | 14 | 3.47 |
Adolfo Duran | 3 | 10 | 3.30 |
Caique Lima | 4 | 0 | 0.34 |
Ademilson Lima | 5 | 0 | 0.34 |