| A Chain Datatype in Z |
| Received:March 08, 2009 Revised:August 16, 2009 Download PDF |
| Leo Freitas,Jim Woodcock. A Chain Datatype in Z. International Journal of Software and Informatics, 2009,3(2):357~374 |
| Hits: 3301 |
| Download times: 2974 |
|
|
| Abstract:We present results about a general-purpose chain datatype specified in the Z notation and mechanised using the Z/Eves theorem prover. Our particular interest comes from its use in the specification and refinement of operating system kernels for embedded real-time devices as part of a pilot project within the international Grand Challenge in Verified Software, and to contribute to the Verified Software Repository. We show—at afairly high level—the sort of dogged work that is needed to get a body of results together to form a basis for future projects. Our work discusses important hidden and missing properties in the specification of the chain datatype and its relation to kernel design. |
| keywords:verified software grand challenge OS kernels |
| View Full Text View/Add Comment Download reader |
|
|
|
