Luca Aceto, Reykjavík University, Iceland
The Saga of the Axiomatization of Parallel Composition
This paper surveys some classic and recent results on the finite axiomatizability of bisimilarity over CCS-like languages. It focuses, in particular, on non-finite axiomatizability results stemming from the semantic interplay between parallel composition and nondeterministic choice. The paper also highlights the role that auxiliary operators, such as Bergstra and Klop's left and communication merge and Hennessy's merge operator, play in the search for a finite, equational axiomatization of parallel composition both for classic process algebras and for their real-time extensions.
Peter O'Hearn, Queen Mary University of London, UK
Separation Logic Semantics for Communicating Processes
not available, yet
Fred B. Schneider, Cornell University, USA
Mapping the Security Landscape: A Role For Language Techniques
Over the last decade, programming language techniques have been applied in non-obvious ways to building secure systems. This talk will not only survey that work in language based security but show that the theoretical underpinnings of programming languages are a good place to start for developing a much needed foundation for software system security.
Vincent Danos, Université Paris 7, France
Rule-based modelling of cellular signalling
Modelling is becoming a necessity in studying biological signalling pathways, because the combinatorial complexity of such systems rapidly overwhelms intuitive and qualitative forms of reasoning. Yet, this same combinatorial explosion makes the traditional modelling paradigm based on systems of differential equations impractical, if not conceptually inappropriate. Agent-based or concurrent languages, such as κ, or the closely related BNG language, offer an alternative where one describes biological interactions by rules, and therefore avoids the combinatorial explosion that plagues the differential approach. Rules are written in an intuitive graphical notation and transparently represent biological knowledge, thereby making models easier to build, discuss, and modify. We illustrate this with a sizeable example obtained by refactoring two differential models of the EGF receptor signalling.
José Luiz Fiadeiro, University of Leicester, UK
Foundations of Service-Oriented Modelling
We report on the work that is being developed within the FP6-IST-FET Integrated Project SENSORIA (www.sensoria-ist.eu) aimed at providing formal support for modelling service-oriented systems in a way that is independent of the languages in which services are programmed and the platforms over which they run. We discuss the semantic primitives that are being provided in the SENSORIA Reference Modelling Language (SRML) for modelling composite services, i.e. services whose business logic involves a number of interactions among more elementary service components as well the invocation of services provided by external parties. This includes a logic for specifying stateful, conversational interactions, a language and semantic model for the orchestration of such interactions, and an algebraic framework supporting service discovery, selection and dynamic assembly.