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


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: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year