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
VerdejoMartí-Oliet00
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)
VerdejoMartí-Oliet02a
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
VerdejoMartí-Oliet02b
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)