Operational Conservative Extension and Bisimulation for Modular SOS

Mark New

(Swansea)

Descriptions written using the Structural Operational Semantics (SOS) framework suffer with poor modularity: extending descriptions often requires extensive reformulation of the rules, which hinders changes and discourages reuse. The Modular SOS (MSOS) framework solves this problem, allowing specifications to be developed that can be extended or reused without reformulation.

We present the first study of proving semantic equivalences based on MSOS. After giving an overview of MSOS, we present a format that ensures that extensions are operationally conservative. We then give definitions of bisimulation for MSOS as well as example proofs based on simple programming language constructs. Finally, we discuss the modularity of these proofs.
Thursday 6th November 2008, 14:00
Robert Recorde Room
Department of Computer Science