[pdf]
In H. Ehrig, M. Grosse-Rhode, and F. Orejas, editors, INT 2000,
Integration of Specification Techniques with Applications in Engineering,
Extended Abstracts Technical report 2000/04, Technische Universitat Berlin,
March 2000, pages 49-53, 2000.
Abstract: Rewriting logic can be used as a semantic framework
where the formal structural operational semantics of specification languages
as E-LOTOS can be described in a easy way. E-LOTOS has been developed within
ISO for the formal specification of open distributed concurrent systems
in general. Its formal semantics has been already defined, but tools need
to be developed in order to show the features of the language, and to check
the correctness of the specifications. By using the rewriting logic language
Maude, not only the E-LOTOS semantic rules can be described, but they can
be executed. Furthermore, due to the rewriting logic reflective capabilities,
properties about the E-LOTOS specifications can be proved in the same framework.
For example, both an E-LOTOS protocol specification and the tool that checks
it by exploring all its behaviours can be implemented by using the Maude
language. This approach has been successfully applied to the Milner's toy
language CCS, defining its semantics and verifying processes written in
that language. The same ideas are being extended to a bigger language such
as E-LOTOS.
@InProceedings{VerdejoMarti-Oliet00b,
author = {Alberto Verdejo and Narciso Mart{\'\i}-Oliet},
title = {Executing {E-LOTOS} processes in {Maude}},
booktitle = {INT 2000, Integration of Specification Techniques with
Applications in Engineering, Extended Abstracts Technical
report 2000/04, Technische Universitat Berlin, March
2000},
pages = {49-53},
year = 2000,
editor = {H. Ehrig and M. Grosse-Rhode and F. Orejas}
}