Invited Speakers
We have the pleasure of announcing the following distinguished speakers who
have kindly accepted our invitation to lecture at iFM 2013:
 JeanRaymond Abrial, Marseille, France: From Z to B and then EventB:
Assigning Proofs to Meaningful Programs
Abstract:
The very first paper on Z was published in 1980, then the book on B
was published in 1996, and, finally, the book on EventB was published in
2010. So, 30 years separate Z from EventB. 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 EventB".
Since I am the main contributor (at least initially) of these three topics
(Z, B, and EventB), 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 EventB, 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 knowledgebased 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 knowledgebased presentation helps achieving the necessary correctness
proofs.
 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 energyaware and
energyharvesting embedded systems. We review these formalisms and
a range of associated decision problems covering costoptimal reachability,
modelchecking and costbounded 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 simulationbased "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 Uppaalsmc, and applied to the performance analysis of a number
of systems ranging from realtime 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 parallelfree finitestate 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
service discovery.

News

1.7.2013
Susanne Graf's pictures from iFM 2013 are now available.

27.6.2013
Videos are now available.

18.6.2013
Photos from all days are now available.

10.6.2013
The detailed schedule of iFM 2013 is here.

10.6.2013
Maps of Turku city and ICTbuilding has been added.

10.6.2013
Social event program updated.

6.6.2013
The Rector of Åbo Akademi University,
Professor Jorma Mattinen will kindly open iFM 2013, on June 12, at 8:45 in
Auditorium Alpha!

4.6.2013
The Åbo Akademi University magazine "Meddelanden" reported (in Swedish)
about iFM 2013 here.

23.05.2013
The proceedings of iFM 2013 (LNCS 7940) is now accessible from Springer, here.

22.4.2013
The schedule and the list of accepted papers (with abstracts) have been uploaded.

26.3.2013
Registration has opened!

11.1.2013
We have extended the paper submission deadline to 27.1.2013!

19.11.2012
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.

12.11.2012
We have the pleasure of confirming the following invited speakers at iFM
2013: JeanRaymond Abrial, Cosimo Laneve, Susanne Graf, and Kim Larsen.

31.10.2012
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.
Archive
