40 Years of Computing at Newcastle
Department Technical Report Series No. 551
Formal Software and Hardware Development: A Case Study in the Use of CSDM, SPECTRUM and HOLCF.
L.J. Steggles and M. Wirsing.
University of Newcastle upon Tyne. 1996
Abstract
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.
Department Technical Report Series - 1996
Department Technical Report Series Index
Contents Page - 40 Years of Computing at Newcastle
Technical Report Abstract No. 551, 30 June 1997