Invited Speakers

Abstracts of Invited Talks

Mining Precise Specifications
Andreas Zeller

Recent advances in software validation and verification make it possible to widely automate the check whether a specification is satisfied. This progress is hampered, though, by the persistent difficulty of writing specifications. Are we facing a "specification crisis"? By mining specifications from existing systems, we can alleviate this burden, reusing and extending the knowledge of 60 years of programming, and bridging the gap between formal methods and real-world software. But mining specifications has its challenges: We need good usage examples to learn expected behavior; we need to cope with the approximations of static and dynamic analysis; and we need specifications that are readable and relevant to users. In this talk, I present the state of the art in specification mining, its challenges, and its potential, up to a vision of seamless integration of specification and programming.

Connector Algebras and Petri Nets
(FME Invited Lecture)
Ugo Montanari
(Joint work with Roberto Bruni, Pisa, and Hernan Melgratti, Buenos Aires)

Recent years have witnessed an increasing interest about a rigorous modelling of (different classes of) connectors. The term "connector", as used here, has been coined within the area of component-based software architectures, to name entities that can regulate the interaction of a collection of components. Thus, connectors must take care of all those aspects that lie outside the scopes of individual components. This has led to the development of different mathematical frameworks that are used to specify, design, analyse, compare, prototype and implement suitable connectors. A rigorous mathematical foundations is crucial for the analysis of coordinated distributed systems. In this talk, we overview the main features of some notable theories of connectors and discuss their similarities, differences, mutual embedding and possible enhancements.

End-to-end Guarantees in Embedded Control Systems
Rupak Majumdar

Software implementations of controllers for physical subsystems form the core of many modern safety-critical systems such as aircraft flight control and automotive engine control. In the model-based approach to the design and implementation of these systems, the control designer starts with a mathematical model of the system and argues that key properties — such as stability and performance — are met for the model. Then, the model is compiled into code, where extensive simulations are used to informally justify that the implementation faithfully captures the model.

We present a methodology and a tool to perform automated static analysis of control system models together with embedded controller code. Our methodology relates properties, such as stability, proved at the design level with properties of the code. Our methodology is based on the following separation of concerns. First, we analyze the controller mathematical models to derive bounds on the implementation errors that can be tolerated while still guaranteeing the required performance. Second, we automatically analyze the controller software to check if the maximal implementation error is within the tolerance bound computed in the first step.

We present two examples of this methodology: first, in verifying bounds on the stability of control systems in the presence of errors arising from the use of fixed-point arithmetic, and second, in generating flexible schedulers for control systems sharing common resources.

Models of Provenance
Peter Buneman

As more and more information is available to us on the Web, the understanding of its provenance -- its source and derivation -- is essential to the trust we place in that information. Provenance has become especially important to scientific research, which now relies on information that has been repeatedly copied, transformed and annotated.

Provenance is also emerging as a topic of interest to many branches of computer science including probabilistic databases, data integration, file synchronization, program debugging and security. Efforts by computer scientists have resulted in a somewhat bewildering variety of models of provenance which, although they have the same general purpose, have very little in common.

In this talk, I will attempt to survey these models, to describe why they were developed and to indicate how they can be connected. There has been a particularly rich effort in describing the provenance of data that results from database queries. There are also emerging models for the description of provenance associated with workflows. Can they, or should they, be reconciled? I shall also talk about some of the practical issues involved in the recording and maintenance of provenance data.

Petri Net Distributability
Eike Best
(Joint work with Philippe Darondeau (INRIA, IRISA, France))

A Petri net is distributed if, given an allocation of transitions to (geographical) locations, no two transitions at different locations share a common input place. A system is distributable if there is some distributed Petri net implementing it.

This talk addresses the question of which systems can be distributed, while respecting a given allocation. The paper states the problem formally and discusses several examples illuminating the current status of this work.