Case Study: A Digital and Analogue Watch

  • John Derrick
  • Eerke Boiten
Part of the Formal Approaches to Computing and Information Technology book series (FACIT)

Abstract

The MD of our local watch manufacturer has decided to use Z to describe the functionality of the latest watches in production. Given an initial abstract specification there are a number of possible implementations, and in this chapter we use a collection of different refinement techniques to verify that the implementations are correct with respect to the initial design.

Keywords

Derrick 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 2001

Authors and Affiliations

  • John Derrick
    • 1
  • Eerke Boiten
    • 1
  1. 1.Computing LaboratoryUniversity of Kent at CanterburyCanterbury, KentUK

Personalised recommendations