Mapping modular SOS to rewriting logic

Christiano De O. Braga, E. Hermann Hæusler, José Meseguer, Peter D. Mosses

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)262-277
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2664
StatePublished - 2003

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Mapping modular SOS to rewriting logic'. Together they form a unique fingerprint.

Cite this