An executable specification of asynchronous pi-calculus semantics and may testing in maude 2.0
By
We describe an executable specification of the operational semantics of an asynchronous version of the π-calculus in Maude by means of conditional rewrite rules with rewrites in the conditions. We also present an executable specification of the may testing equivalence on non-recursive asynchronous π-calculus processes, using the Maude metalevel. Specifically, we describe our use of the metaSearch operation to both calculate the set of all finite traces of a non-recursive process, and to compare the trace sets of two processes according to a preorder relation that characterizes may testing in asynchronous π-calculus. Thus, in both the specification of the operational semantics and the may testing, we make heavy use of new features introduced in version 2.0 of the Maude language and system.
BibTeX
@article{journals/entcs/ThatiSM02, author = "Thati, Prasanna and Sen, Koushik and Martí-Oliet, Narciso", title = "An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in Maude 2.0", ee = "http://dx.doi.org/10.1016/S1571-0661(05)82539-3", journal = "Electr. Notes Theor. Comput. Sci", keywords = "formal methods", pages = "261-281", volume = "71", year = "2002", }