Paper Details

Development of an ML based Verification Tool for Timed CSP Processes

Authors: Yamakawa, Takeshi, Ohashi, Tsuneki, Fukunaga, Chikara

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.

Proceedings:

Communicating Process Architectures 2011, Peter H. Welch, Adam T. Sampson, Jan Bækgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes, 2011, pp 363 - 375 published by IOS Press, Amsterdam

Files: Paper (PDF), Slides (PDF)

This record in other formats:

Web page: BibTEX, Refer
Plain text: BibTEX, Refer

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.