We have the pleasure of announcing the following distinguished speakers who
have kindly accepted our invitation to lecture at iFM 2013:
- Jean-Raymond Abrial, Marseille, France: From Z to B and then Event-B:
Assigning Proofs to Meaningful Programs
The very first paper on Z was published in 1980, then the book on B
was published in 1996, and, finally, the book on Event-B was published in
2010. So, 30 years separate Z from Event-B. It is thus clear that I spent a
significant time of my scientific professional life working with the same kind of subject in
mind, roughly speaking specification language and program verification.
So, I was very pleased when the organizer of iFM 2013, Luigia Petre and
Einar Broch Johnsen, invited me to give a talk at the conference and at the
same time suggested that I can give a presentation on "Z to Event-B".
Since I am the main contributor (at least initially) of these three topics
(Z, B, and Event-B), there are certainly some common features that are
interesting to put forward in the three of them. But at the same time, during these
thirty years, it was also possible to gradually envisage some evolution from the
first to the last. The main purpose of this presentation is thus to clarify this. This paper
does not contain a description of Z, B, or Event-B, as well as that of the
corresponding tools that have been developed over the years. Readers interested by this
can access the literature. In the main part of the paper, I rather present a historical account. The
idea is to explain how all this has slowly emerged as an intellectual
evolution. I will also try to make clear what are the external ideas and events (there
are many) that influenced this evolution. Then I will try to make a synthesis
and present what is common in these three topics and also what makes them
different from each other. This will take place in two Appendices.
- Susanne Graf, VERIMAG, France: Knowledge for the Distributed Implementation of Constrained Systems
Abstract: Deriving distributed implementations from global
specifications has been extensively studied for different application domains, under different
assumptions and constraints. We explore here the knowledge perspective: a process
decides to take a local action when it has the knowledge to do so. We
discuss typical knowledge atoms that are useful for expressing local enabling
conditions with respect to different notions of correctness, as well as different means
for obtaining knowledge and for representing it locally in an efficient manner.
Our goal is to use such a knowledge-based representation of the distribution
problem for either deriving distributed implementations automatically from global
specifications on which some constraint is enforced, or for improving the efficiency
of existing protocols by exploiting local knowledge. We also argue that such
a knowledge-based presentation helps achieving the necessary correctness
- Kim Larsen, Aalborg University, Denmark: Priced Timed Automata and Statistical Model Checking
Abstract: The notions of priced timed automata (PTA) and energy
games (EG) provide useful modeling formalisms for energy-aware and
energy-harvesting embedded systems. We review these formalisms and
a range of associated decision problems covering cost-optimal reachability,
model-checking and cost-bounded infinite strategies. Decidability of
several of these problems require tight bounds on the number of clocks
and cost variables. Thus, we turn to statistical model checking (SMC),
which has emerged as a highly scalable simulation-based "approximate"
validation technique. In a series of recent work we have developed a natural
stochastic semantics for PTAs allowing for statistical model checking
to be performed. The resulting techniques have been implemented
in Uppaal-smc, and applied to the performance analysis of a number
of systems ranging from real-time scheduling, mixed criticality systems,
sensor networks, energy aware systems and systems biology.
- Cosimo Laneve, University of Bologna, Italy: An Algebraic Theory for Web Service Contracts
Abstract: We study a natural notion of compliance between clients
and services in terms of their BPEL (abstract) descriptions. The induced
preorder shows interesting connections with the must preorder and has
normal form representatives that are parallel-free finite-state activities,
called contracts. The preorder also admits the notion of least service
contract that is compliant with a client contract, called principal dual
contract. Our framework serves as a foundation of Web service tech-
nologies for connecting abstract and concrete service definitions and for
Susanne Graf's pictures from iFM 2013 are now available.
Videos are now available.
Photos from all days are now available.
The detailed schedule of iFM 2013 is here.
Maps of Turku city and ICT-building has been added.
Social event program updated.
The Rector of Åbo Akademi University,
Professor Jorma Mattinen will kindly open iFM 2013, on June 12, at 8:45 in
The Åbo Akademi University magazine "Meddelanden" reported (in Swedish)
about iFM 2013 here.
The proceedings of iFM 2013 (LNCS 7940) is now accessible from Springer, here.
The schedule and the list of accepted papers (with abstracts) have been uploaded.
Registration has opened!
We have extended the paper submission deadline to 27.1.2013!
We are very happy to announce that the following TWO renowned Springer
journals have kindly accepted to host special issues of iFM 2013: Formal
Aspects of Computing and Software and Systems Modeling.
We have the pleasure of confirming the following invited speakers at iFM
2013: Jean-Raymond Abrial, Cosimo Laneve, Susanne Graf, and Kim Larsen.
We have now booked the lovely venue of Herrankukkaro for the
social event on 13.6.2013. We will go to a fishing village close to Turku,
where we will walk around, take a (smoke) sauna, and enjoy a
nice dinner. We will go there
by bus and come back by boat, enjoying the light nights of June in Finland. You can check more about it here.