Automatically Generating CSP Models for Communicating Haskell Processes

Brown, Neil C.C. (2009) Automatically Generating CSP Models for Communicating Haskell Processes. In: Automated Verification of Critical Systems 2009 (AVOCS09), September 23rd - 25th, 2009 , Swansea. (Full text available)

PDF - Publisher pdf
Download (170kB) Preview
[img]
Preview

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: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Neil Brown
Date Deposited: 08 May 2013 15:01 UTC
Last Modified: 12 May 2014 16:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/33866 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year