A Chain Datatype in Z
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

Leo Freitas, Jim Woodcock. A Chain Datatype in Z. International Journal of Software and Informatics, 2009,3(2):357~374

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 08,2009
  • Revised:August 16,2009
  • Adopted:
  • Online:
  • Published: