[pdf]
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.
Abstract: We explore the features of rewriting logic and the
language Maude as a logical and semantic framework for representing both
the semantics of CCS, and a modal logic for describing local capabilities
of CCS processes. Although a rewriting logic representation of the CCS
semantics was given previously, it cannot be directly executed in the 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 the 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 by exploiting the reflective
properties of rewriting logic, which allow controlling the rewriting process.
This executable specification plus the reflective control of the rewriting
process can be used to analyze CCS processes.
@InProceedings{VerdejoMarti-Oliet00c,
author = {Alberto Verdejo and Narciso Mart{\'\i}-Oliet},
title = {Implementing {CCS} in {Maude}},
booktitle = {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},
year = {2000},
editor = {Tommaso Bolognesi and Diego Latella},
publisher = {Kluwer Academic Publishers}
}