Formal Software and Hardware Development: A Case Study in the Use of CSDM, SPECTRUM and HOLCF (1996)

Author(s): L.J. Steggles and M. Wirsing

Abstact: We present a simple methodology for the formal verification of software and hardware systems using algebraic specification methods. This methodology is based on the notion of functional refinement and we define the conditions necessary for a design specification to be a correct functional refinement of an abstract requirement specification. In particular we consider facilitating the reuse of design specifications and the role of the environment information contained within the requirement specification during the verification process. We demonstrate our verification methodology by considering the formal verification of two systolic algorithms for computing the convolution function. This case study is carried out within the CSDM software development environment using the specification language SPECTRUM and the theorem prover Isabelle with the object logic HOLCF.