TY - JOUR
T1 - Mapping modular SOS to rewriting logic
AU - Braga, Christiano De O.
AU - Hæusler, E. Hermann
AU - Meseguer, José
AU - Mosses, Peter D.
PY - 2003
Y1 - 2003
N2 - Modular SOS (MSOS) is a framework created to improve the modularity of structural operational semantics specifications, a formalism frequently used in the fields of programming languages semantics and process algebras. With the objective of defining formal tools to support the execution and verification of MSOS specifications, we have defined a mapping, named MtoR, from MSOS to rewriting logic (RWL), a logic which has been proposed as a logical and semantic framework. We have proven the correctness of MtoR and implemented it as a prototype, the MSOS-SL Interpreter, in the Maude system, a high-performance implementation of RWL. In this paper we characterize the MtoR mapping and the MSOS-SL Interpreter. The reader is assumed to have some basic knowledge of structural operational semantics and object-oriented concepts.
AB - Modular SOS (MSOS) is a framework created to improve the modularity of structural operational semantics specifications, a formalism frequently used in the fields of programming languages semantics and process algebras. With the objective of defining formal tools to support the execution and verification of MSOS specifications, we have defined a mapping, named MtoR, from MSOS to rewriting logic (RWL), a logic which has been proposed as a logical and semantic framework. We have proven the correctness of MtoR and implemented it as a prototype, the MSOS-SL Interpreter, in the Maude system, a high-performance implementation of RWL. In this paper we characterize the MtoR mapping and the MSOS-SL Interpreter. The reader is assumed to have some basic knowledge of structural operational semantics and object-oriented concepts.
UR - http://www.scopus.com/inward/record.url?scp=35248879236&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35248879236&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:35248879236
SN - 0302-9743
VL - 2664
SP - 262
EP - 277
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -