Paper Details

Communicating Process Architectures (CPA)
 Title: Development of an ML based Verification Tool for Timed CSP Processes
 Conference: Communicating Process Architectures 2011
 Authors: Takeshi Yamakawaa, Tsuneki Ohashib, Chikar Fukunagaa
(a) Tokyo Metropolitan University
(b) Tokyo Metropolitan University,
 Abstract: We report the development of a verification tool for Timed CSP processes. The tool has been built on the functional programming language ML. The tool interprets processes described in both timed and untimed CSP, converting them to ML functions, and executing those functions for the verification of refinement in the timed traces and timewise traces models. Using the programmability of higher order functionality, the description of CSP processes with ML has been synthesised naturally. The effectiveness of the tool is demonstrated with an example analysing implementations of Fischer's algorithm for the exclusive control of a shared resource in a multi-processor environment. 
Files:


BibTeX Entry


Full paper


Presentation