ePrints

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

Lookup NU author(s): Dr Jason Steggles

Downloads

Full text is not currently available for this publication.

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.

Publication metadata

Author(s): Steggles LJ, Wirsing M

Publication type: Report

Publication status: Published

Series Title: Department of Computing Science Technical Report Series

Year: 1996

Pages: 50

Print publication date: 01/01/1996

Source Publication Date: 1996

Report Number: 551

Institution: Department of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/551.pdf

Share