CCS case study

Executing and Verifying CCS in Maude

We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. The basic idea of the kind of representation used is that judgments in the inference system are represented as terms in Maude, and inference rules are mapped to rewrite rules. In order to illustrate the general ideas, we have represented both the semantics of Milner's CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics was given previously [Marti-OlietMeseguer93], it cannot be directly executed in the current default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic.

Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by exploiting the reflective properties of rewriting logic, which allow controlling the rewriting process. We also show how the semantics can be extended to traces of actions and to the CCS weak transition relation. This executable specification plus the reflective control of the rewriting process can be used to analyze CCS processes.
Maude 1.5 Specifications and Samples

CCS and Modal Logic specification and search strategy

Sample runs

Verdejo, A., Martí-Oliet, N. Implementing CCS in Maude. In T. Bolognesi and D. Latella, editors, Formal Methods For Distributed System Development. FORTE/PSTV 2000 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX) October 10-13, 2000, Pisa, Italy, pages 351-366. Kluwer Academic Publishers, 2000. (gzip'ped ps)

Verdejo, A., Martí-Oliet, N. Executing and Verifying CCS in Maude. Submitted for publication, October 2002. (gzip'ped ps)

Implementing CCS in Maude 2

The recent availability of implementations for Maude 2.0 have made it possible to consider a different approach where CCS transitions are represented as rewrites and the inference rules are mapped to conditional rules with rewrites in the conditions. That has been possible because Maude 2.0 allows indeed conditional rules with rewrites in the conditions, where those rewrites are solved at execution time by means of a built-in search mechanism. Thus, we have been able to undertake a continuation of our previous project by carefully reimplementing in a fully \emph{executable} way the CCS operational semantics considering transitions as rewrites. We have implemented both the usual transition semantics and the weak transition semantics where internal actions are not observed, and on top of them we also implement the Hennessy-Milner modal logic for describing processes. The paper below describes in detail the results obtained in this second implementation and compares both implementations.
Maude 2.0 Specifications and Samples

CCS and Modal Logic specification and examples

 Verdejo, A., Martí-Oliet, N. Implementing CCS in Maude 2. In F. Gadducci and U. Montanari, editors, Proceedings Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, volume 71 of Electronic Notes in Theoretical Computer Science, pages 239-257. Elsevier, 2002. (gzip'ped ps)

[Maude Home Page]