Skip to main content

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)

PDF Publisher pdf
Language: English
Click to download this file (197kB) Preview
[thumbnail of CHP-Models.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:
http://dx.doi.org/10.14279/tuj.eceasst.23.325.320

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)
  • Depositors only (login required):

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