Automatically Generating CSP Models for Communicating Haskell Processes
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.
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.23.325
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.23.325.320
Hosted By Universitätsbibliothek TU Berlin.