Abstract
In this report we present a simulator CMRsim for the Copyable Mobile Resources Calculus (CMR). We implement a lexer and parser for the full calculus and provide methods to compare expressions for structural congruence, and methods to find and execute reductions of CMR expressions.
We present CMRmin, a restricted version of CMR, that allows equivalence testing to be performed by introducing a finite transition system. We implement a checking algorithm for strong bisimulation for CMRmin.
We describe the implemented simulator and the theory relevant to the implementation. The bisimulation algorithm is implemented by an algorithm for solving the Partition Refinement Problem.
Keywords: Copyable Mobile Resources, Bisimulation, Interpreter, process calculi, partition refinement.
Introduction
This is a 4-week project (7.5 ECTS) written on the 4th semester of the Master of Science program Internet and Software Technology at the IT University of Copenhagen.
The focus of this report has been on the implementation of a equivalence checker for Copyable Mobile Resources (CMR). As such, much of the time available for this project was spent programming and working with the calculus.
Our motivation for making this project was to work with an abstract model for mobile computation and to apply knowledge gained from a course in programming languages.
Since this is our first try at an larger program in Standard ML some of the code is somewhat inept and only uses some of the ``possibilities'' that Standard ML provides. Our code currently runs under the Moscow ML SML implementation Version 2.00.
Furthermore the implemented algorithms in this project should be seen as proof of concept and work in progress, rather than an attempt at an efficient implementation of a model checker for CMR.
We assume that the reader has a basic knowledge of process algebra and the theories behind models for concurrent and mobile computation. Also, we assume that the reader has a basic knowledge of parsing theory, including abstract syntax trees and context-free grammar. Knowledge of functional programming languages will also benefit the reader.
Download
Project:
The report (in pdf)
377 KB