Some titles and abstracts for talks IFIP WG
2.2 Anniversary Meeting
(in alphabetical order)
Speaker: Egon Boerger
Title: Contributions of the Abstract State Machines method to program verification
and some future challenges
Abstract: We first survey applications of the ASM
method for a rigorous definition and mathematical analysis of the semantics
of modern programming languages and their implementation. Then we discuss some
contributions the ASM method can provide to address the Verified Software Grand
Challenge proposed by T. Hoare.
Speaker: Philippe Darondeau
Title: Petri net synthesis 10 years later
Abstract: We survey results and applications found
in the last decade in the field of Petri net synthesis. We present current trends
of research and open problems.
Speaker: Mariangiola Dezani
Title: Session Types
for Object-Oriented Languages
Abstract: A session takes place between two parties;
after establishing a connection, each interleaves local computations and communications
(sending or receiving) with the other. Session types characterise such sessions
in terms of the types of values communicated and the shape of protocols, and
have been developed for the pi-calculus, CORBA interfaces, and functional languages.
We study the incorporation of session types into object-oriented languages through
MOOSE, a multi-threaded language with session types, thread spawning, iterative
and higher-order sessions. Our design aims to consistently integrate the object-oriented
programming style and sessions, and to be able to treat various case studies
from the literature. We describe the design of MOOSE, its syntax, operational
semantics and type system, and develop a type inference system. After proving
subject reduction, we establish the progress property: once a communication
has been established, well-typed programs will never starve at communication
points. (Joint work with Dimitris Mostrous, Nobuko Yoshida and Sophia Drossopoulou)
Speaker: Furio Honsell
Title: A Framework for Defining Logical Frameworks
Speaker:
Maciej Koutny
Title: Verifying Mobile Systems Using Petri Net Unfoldings
Abstract:
To make formally express and analyse mobile systems feasible, process algebras
- notably the pi-calculus - have been introduced and extensively studied. This
talk will describe how one can apply Petri net unfoldings in order to alleviate
the state space explosion problem when model checking systems expressed in the
finite pi-calculus.
Speaker: Leslie Lamport
Title: A State Machine by any Other Name
Abstract: Much of computer science is about state machines, known by a
multitude of names: automata (Buchi, cellular, pushdown), machines (Mealy, Moore,Turing),
programs, Petri nets, process algebras, and so on. What are the significant
differences among them all? Are state machines all you need?
Speaker: Hans Langmaack
Title: Revival of ALGOL-Concepts in Program and Specification Languages
Abstract:
In recent years there have happened extensions of two very respected and widely
used programming and specification languages: The extension from original, object
oriented, flat Java 1996 to new Java 2000 with class nesting (Gosling, Joy,
Steele, Bracha) and from basic Abstract State Machines ASMs 1986/90 to Turbo
ASMs 2002 (Gurevich, Boerger, Stark). These extensions are well comparable to
the much earlier transition from Fortran 1954/57 (Backus) and Algol58, 1958
(Perlis, Samelson, Paul) to Algol60, 1960 (Naur et al.). It is Algol60's concept
of program structuring, information encapsulation and hiding by the help of
nested, non-formal and formal procedures with their static scope semantics the
revival of which we detect under quite different namings both in new Java and
in Turbo ASM.
Speaker: Marino Miculan
Title: Modal Logics for Brane Calculus
Abstract: The Brane Calculus is a calculus of mobile processes, in- tended to
model the transport machinery of a cell system. We present the Brane Logic,
a modal logic for expressing formally properties about systems in Brane Calculus.
Similarly to previous logics for mobile ambients, Brane Logic has specific spatial
and temporal modalities. Moreover, since in Brane Calculus the activity resides
on membrane surfaces and not inside membranes, we need to add a specific logic
(akin Hennessy-Milner's) for reasoning about membrane activity. We provide also
a proof system for deriving valid sequents in Brane Logic, and a model checker
for a decidable fragment.
Speaker: Ugo Montanari
Title: A Larger Viewpoint about Leifer and Milner's Reactive Systems
Abstract: A systematic method for deriving
bisimulation congruence from reduction rules has been proposed by Leifer and
Milner, on turn inspired by Sewell. Also, the approach of observing contexts
imposed on agents at each step has been proposed earlier by Montanari and Sassone,
yielding the notion of dynamic bisimilarity. The basic idea of Leifer and Milner
is to express minimality conditions for electing the context to be used among
the (possibly infinite) ones that allow the agent to react. These conditions
have been distilled by them in the notion of relative push-out (RPO) in a categories
of reactive systems and made more general by Sassone, Sobocinski and Lack. The
RPO construction is reminiscent of the unification process of logic programming,
which in fact can be given an interactive semantics in much the same style.
In the talk we present a short survey of the relevant work and describe some
recent developments which allow to see this approach under a larger viewpoint.
The first contribution observes contexts also for symbolic execution, suggesting
applications to web service binding; the second tackles the weak case by taking
advantage of the tile model; and the third uses cospan categories on adhesive
categories, as suggested by Sassone, Sobocinski and Lack, for representing process
calculi as graph transformation systems. As a last contribution, we then propose
saturated semantics, a new class of equivalences, based on a weaker notion of
observation and orthogonal to all the previous proposals, and we demonstrate
the appropriateness of our semantics by means of two examples: logic programming
and a subset of the open pi-calculus. Indeed, we show that our equivalences
are congruences and that they coincide with logical equivalence and open bisimilarity
respectively, while equivalences studied in previous work are strictly finer
(Joint work with Filippo Bonchi, Roberto Bruni, Gianluigi Ferrari, Fabio Gadducci,
Barbara Koenig, Pawel Sobocinski and Emilio Tuosto).
Speaker: Peter D. Mosses
Title: Formal semantics online
Abstract: Over the past 40 years, various formalisms
for semantics have been developed - often by past or present members of WG 2.2
- and used to give semantic descriptions of some major programming languages.
However, it appears that rather few semantic descriptions are currently available
online. A comprehensive online archive of existing semantic descriptions would
surely be a valuable resource in itself, and enhance the visibility of formal
semantics in the computer science community. In this talk, we outline a new
initiative to establish such an archive. We also consider the possibility of
incorporating canonical descriptions of commonly-occurring individual constructs,
which could serve as reusable components for future semantic descriptions.
Speaker:
Ernst-Rudiger Olderog
Title: Automatic Verification of Combined Specifications
Abstract: In our talk we report on the project "Beyond Timed Automata" (R1 for
short) of the Collaborative Research Center AVACS (Automatic Verification and
Analysis of Complex Systems) of the universities of Oldenburg, Freiburg, and
Saarbr"ucken. AVACS is motivated by the challenge of automatically verifying
safety properties of complex embedded systems like the European Train Control
System (ETCS). The long term vision of R1 is to advance the automatic verification
of high-level specifications in the dimensions of behaviour, data, and real-time.
The current emphasis in R1 is on the automatic verification of specifications
with infinite data and real-time constraints. In R1 we consider for the specifications
of systems the language CSP-OZ-DC that combines three well researched specification
techniques for processes, data and time: Communicating Sequential Processes
(CSP), Object-Z (OZ), and Duration Calculus (DC). For the specifying real-time
requirements we take the Duration Calculus. The combination CSP-OZ-DC has an
operational semantics defined by J. Hoenicke in terms of Phase-Event-Automata
(PEA). This semantics is compositional in the sense that the automaton describing
the set of runs a combined CSP-OZ-DC specification is the parallel composition
of the automata for the CSP part, the OZ part, and the DC part. Automatic verification
of CSP-OZ-DC specifications is achieved using the Abstraction Refinement Model
Checker (ARMC) of A. Rybalchenko. It uses transition constraint systems as input
and can check the the reachability of set of states. In its current implementation
it can handle constraints on data in the domains of real and integer numbers.
PEA are very well suited as an intermediate language in translating CSP-OZ-DC
specifications into transition constraint systems processed by ARMC. In the
talk we illustrate the approach using the example of a parameterized elevator
studied by J. Hoenicke and P. Maier. The point is that a safety property of
the lift depending on real-time constraints in its CSP-OZ-DC specification can
be proven automatically for arbitrarily many floors. Finally, we explain the
status of a larger case study Emergency Messages of the ETCS. Acknowledgement.
The project R1 is directed by A. Podelski, B. Finkbeiner, V. Sofroni-Stokkermans,
and myself. The results reported in this talk build on further work of I. Br"uckner,
J. Faber, J. Hoenicke, R. Meyer, P. Maier, A. Rybalchenko, S. Jacobs, and H.
Wehrheim. For more information about AVACS see the web page www.avacs.org.
Speaker:
Catuscia Palamidessi
Title: Anonymity Protocols as Noisy Channels
Abstract:
We propose a framework in which anonymity protocols are interpreted as particular
kinds of channels, and the degree of anonymity provided by the protocol as the
converse of the channel's capacity. We illustrate how several notions of anonymity
can be expressed in this framework, and show the relation with various definitions
of probabilistic anonymity in literature. (Joint work with Kostas Chatazikokolakis,
Prakash Panangaden)
Speaker: Gordon Plotkin
Title: Origins of structural operational semantics
Speaker: Andrzej Tarlecki
Title: Toward (institutional) foundations
for heterogeneous specifications
Abstract: The overall idea of the talk is to
present recent work aimed at dealing with multiple logical systems in a single
specification and software development task. I first recall the basic technical
notions related to modelling logical systems as institutions, and mention a
number of exciting possibilities for applications of the theory of institutions.
Then I sketch how the mechanisms of various mappings between institutions may
be used to cater for heterogeneous specifications, which span an number of linked
institutions, and for the description of the development process which may 'migrate'
between various institutions in the course of development of separate modules
of the system. I will introduce a concept of a distributed heterogeneous specification,
which captures different views of the same system to be developed and briefly
suggest how such distributed specifications can be used in the process of sofwtare
development. Overall, a picture of a heterogeneous logical environment for software
specification and development is emerging as a diagram of institutions linked
by morphisms of various kinds.
Speaker: Igor Walukiewicz
Title: From logic to games
Abstract: In this talk we will look at some developments in what is called
formal verification. In the seventies logics occupied a principal place: Hoare
logic, algorithmic logic, dynamic logic, linear time temporal logic. With a
notable exception of the last one, these formalisms included programs into syntax
of the logic with an idea to reduce verification to validity checking. Temporal
logic was the first to advocate externalization of modeling of programs and
passing from validity checking to model checking. Since the eighties, this view
became predominant, and we have seen a proliferation of logical systems. On
the way, we have learned that game based methods not only are very useful but
also permit to abstract from irrelevant details of logical formalisms. At present
games themselves take the place of specification formalisms.