July 6, 2008, Reykjavik, Iceland
| Invited Speaker | Title/Abstract |
|---|---|
| Vincent Danos | A stochastic calculus of binding - applications to the modelling of cellular signalling |
TBA | |
| Dale Miller | Formalizing SOS specifications in logic |
SOS specifications are generally viewed as inductive definitions in the sense of, say, Smullyan's Formal Systems. Encoding such specifications as logical theories can provide the formalization of semantic specifications many advantages, especially since logic and the theory of proofs have a long tradition of dealing with rich forms of abstractions and bindings. Logical quantifiers can clarify the roles of and interactions between schema variables, bound variables, and constants. Standard automated reasoning tools can also be used to animate many SOS specifications. In this talk, I will focus on using logic to reason directly with SOS specifications encoded as logical theories and will use the pi-calculus as an example. We also show how logical considerations can lead to a natural generalization of the tyft/tyxt rule format to deal with mobility in process calculi. | |
|
Joseph Sifakis
(joint speaker with ICE'08) | Component-based construction of heterogeneous real-time systems in BIP |
We present a framework for the component-based construction of real-time systems. The framework is based on the BIP (Behavior, Interaction, Priority) semantic model, characterized by a layered representation of components. Compound components are obtained as the composition of atomic components specified by their behavior and interface, by using connectors and dynamic priorities. Connectors describe structured interactions between atomic components, in terms of two basic protocols: rendezvous and broadcast. Dynamic priorities are used to select amongst possible interactions - in particular, to express scheduling policies. BIP supports a methodology for incremental construction within a three-dimensional space: Behavior × Interaction × Priority. The separation between behavior and architectural constraints expressed by interactions and priorities, eases compositional verification of systems through a separate analysis of their atomic components and their architectural constraints. The BIP framework has been implemented in a language and a toolset. The BIP language offers primitives and constructs for modelling and composing atomic components described as state machines, extended with data and functions in C. The BIP toolset includes an editor and a compiler for generating from BIP programs, C++ code executable on a dedicated platform. It allows simulation and verification of BIP programs by using model checking or compositional techniques for some properties such as deadlock-freedom. We provide several examples illustrating the use of BIP for modeling heterogeneous systems. Further information is available at http://www-verimag.imag.fr/~async/bip.php. |
| Moderator(s) | Title/Abstract |
|---|---|
| Michel A. Reniers, MohammadReza Mousavi | Towards a textbook on Structural Operational Semantics |
The discussion is about the possibilities of producing a textbook on Structured Operational Semantics. The book can be used for teaching purposes and shows of the achievements of this field to those that arrive anew in research and development (master students and PhD students). Questions that may be answered during the discussion are the following:
|
| Author(s) | Title/Abstract |
|---|---|
|
Eike Best, Kerstin Strecker | Relational semantics revisited |
This paper describes the systematic use of fixpoints for the relational semantics of unboundedly nondeterministic sequential programs. The focus is on analysing the expressiveness of various semantic definitions and of powerdomains including an 'error' element. | |
|
Rocco De Nicola, Diego Latella, Michele Loreti, Mieke Massink | MarCaSPiS: a Markovian extension of a calculus for services |
Service Oriented Computing (SOC) is a design paradigm that has evolved from earlier paradigms including object-orientation and component-based software engineering. Important features of services are compositionality, context-independence, encapsulation and re-usability. To support the formal design and analysis of SOC applications recently a number of Service Oriented Calculi have been proposed. Most of them are based on process algebras enriched with primitives specific of service orientation such as operators for manipulating semi-structured data, mechanisms for describing safe client-service interactions, constructors for composing possibly unreliable services and techniques for services query and discovery. In this paper we show a versatile technique for the definition of Structural Operational Semantics of MarCaSPiS, a Markovian extension of one of such calculi, namely the Calculus of Sessions and Pipelines, CaSPiS. The semantics deals in an elegant way with a stochastic version of two-party synchronisation, typical of a service-oriented approach, and with the problem of transition multiplicity while preserving highly desirable mathematical properties such as associativity and commutativity of parallel composition. We also show how the proposed semantics can be naturally used for defining a bisimulation-based behavioural equivalence for MarCaSPiS terms that induces the same equalities as those obtained via Strong Markovian Equivalence. | |
|
Peter D. Mosses, Mark J. New | Implicit propagation in Structural Operational Semantics |
In contrast to a transition system specification in process algebra, a structural operational semantics (SOS) of a programming language usually involves auxiliary entities: stores, environments, etc. When specifying SOS rules, particular auxiliary entities often need to be propagated unchanged between premises and conclusions. The standard technique is to make such propagation explicit, using variables. However, referring to all entities that need to be propagated unchanged in each rule can be tedious, and it hinders direct reuse of rules in different language descriptions. This paper proposes a new interpretation of SOS rules, such that each auxiliary entity is implicitly propagated in all rules in which it is not mentioned. The main benefits include significant notational simplification of SOS rules and much-improved reusability. This new interpretation of SOS rules is based on the same foundations as Modular SOS, but avoids the notational overhead of grouping auxiliary entities together in labels. After motivating and explaining implicit propagation, the paper considers the foundations of SOS and Modular SOS specifications, and defines the meaning of SOS specifications with implicit propagation by translating them to Modular SOS. It then shows how implicit propagation can simplify various rules found in the SOS literature. | |
|
Gustavo A. Ospina, Baudouin Le Charlier | Formalisation of C language interfaces |
In practical computing, implementations of programming languages provide an interface that allow programs written in a language to call code written in another programming language, most often C. Usually, those language interfaces are left out of the formal definition of the language, and reasoning about multi-language programs is very difficult due to the lack of precise specifications for the language interfaces. In this paper, we present an application of a framework for the interoperability of programming languages, in which we specified in a systematic way the C interface of a real, rule-based programming language. Our framework is based on simple combinations of the small-step operational semantics of programming languages. We give the main elements of a small-step semantics for the C programming language that can be used to specify the same kind of interfaces for other programming languages implemented in C. | |
| Muck van Weerdenburg | Automating soundness proofs |
When developing a new language with semantics described by Structural Operational Semantics (SOS), one often wants an axiomatisation of this language (w.r.t. to some equivalence) as well. We describe a method for automating the straightforward soundness proofs for the axioms of such an axiomatisation. | |
|
Muck van Weerdenburg, Michel A. Reniers | Structural Operational Semantics with First-Order Logic |
We define a formalism for Structural Operational Semantics (SOS) with first-order-logic formulas as premises. It is shown that in most uses (including all practical uses) this formalism has the same expressivity as SOS without first-order logic. Furthermore, we give a congruence format for (strong) bisimilarity. The latter is shown to be strongly related to the ntyft/ntyxt format. |