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: 3015
Download times: 2493
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



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号