iFM 2013

Invited Speakers

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

    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 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 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 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 service discovery.


  • 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 ICT-building 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: Jean-Raymond 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.