Dynamic structural operational semantics
From MaRDI portal
Abstract: We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades, for upgrading software code during run-time. Dynamic SOS (DSOS) is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and program execution constructs. The important feature of Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the program execution code from the additional (data) structures needed at run-time. In DSOS we aim to achieve the same modularity and decoupling for dynamic software upgrades. This is partly motivated by the long term goal of having machine-checkable proofs for general results like type safety. We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus. As a side result we define of a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation in the Creol setting of concurrent object-oriented programming with active objects and asynchronous method calls.
Recommendations
Cites work
- scientific article; zbMATH DE number 997344 (Why is no real title available?)
- scientific article; zbMATH DE number 107664 (Why is no real title available?)
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- scientific article; zbMATH DE number 944097 (Why is no real title available?)
- scientific article; zbMATH DE number 6148924 (Why is no real title available?)
- scientific article; zbMATH DE number 1418328 (Why is no real title available?)
- A Complete Guide to the Future
- A Distributed Pi-Calculus
- A foundation for actor computation
- A model of cooperative threads
- A model of cooperative threads
- A syntactic approach to type soundness
- Algebraic meta-theory of processes with data
- Algebraic properties for free!
- An evaluation of interaction paradigms for active objects
- An overview of the K semantic framework
- Compositionality of Hennessy-Milner logic by structural operational semantics
- Creol: A type-safe object-oriented model for distributed concurrent systems
- Formal Methods for Components and Objects
- Implicit propagation in structural operational semantics
- MULTILISP: a language for concurrent symbolic computation
- Maude: specification and programming in rewriting logic
- Mobile ambients
- Modular bisimulation theory for computations and values
- Modular semantics for transition system specifications with negative premises
- Modular structural operational semantics
- Mutatis mutandis: safe and predictable dynamic software updating
- Notions of bisimulation and congruence formats for SOS with data
- Object-oriented specification and open distributed systems
- Ott: Effective tool support for the working semanticist
- Resource access control in systems of mobile agents
- Rewriting logic and its applications. 10th international workshop, WRLA 2014, held as a satellite event of ETAPS, Grenoble, France, April 5--6, 2014. Revised selected papers
- SOS formats and meta-theory: 20 years after
- Software Evolution
- Structural operational semantics.
- The semantics of future and an application
- Transitions and trees. An introduction to structural operational semantics.
- Turning SOS rules into equations
Cited in
(2)
This page was built for publication: Dynamic structural operational semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2329443)
