Skip to main content
Kent Academic Repository

Automatically Generating CSP Models for Communicating Haskell Processes

Brown, Neil C.C. (2009) Automatically Generating CSP Models for Communicating Haskell Processes. Electronic Communications of the EASST, 23 . pp. 1-12. ISSN 1863-2122. (doi:10.14279/tuj.eceasst.23.325.320) (KAR id:33866)

Abstract

Tools such as FDR can check whether a CSP model of an implementation is a refinement of a given CSP specification. We present a technique for generating such CSP models of Haskell implementations that use the Communicating Haskell Processes library. Our technique avoids the need for a detailed semantics of

the Haskell language, and requires only minimal program annotation. The generated CSP-M model can be checked for deadlock or refinements by FDR, allowing easy use of formal methods without the need to maintain a model of the program implementation alongside the program itself.

Item Type: Article
DOI/Identification number: 10.14279/tuj.eceasst.23.325.320
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Neil Brown
Date Deposited: 08 May 2013 15:01 UTC
Last Modified: 16 Nov 2021 10:11 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/33866 (The current URI for this page, for reference purposes)

University of Kent Author Information

Brown, Neil C.C..

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.