ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS)


Home Page


Recent and Forthcoming Events (updated 12/01/30)

Table of contents

1.      ERCIM's oldest active Working Group

Following an initial successful workshop bringing together ERCIM members interested in formal verification, held in Pisa in December 1992, Stefania Gnesi and Diego Latella, CNR, Pisa, proposed to create an ERCIM working group dedicated to Formal Methods for Industrial Critical Systems (FMICS). Although at that time, model checking was in its early days, the early ERCIM FMICS community was already aware of the great potential of formal verification techniques.

Since then, the WG, chaired in succession by Diego Latella (ISTI-CNR), Hubert Garavel (INRIA), Stefania Gnesi (ISTI), Pedro Merino (SparCIM), Alessandro Fantechi (ISTI), and Radu Mateescu (INRIA), has kept pace with the development of formal verification techniques - and model checking in particular. The series of annual workshops, began in 1996 and sponsored by the WG, have promoted an ongoing scientific discussion focussed on identifying the most efficient verification techniques, with a keen eye to their industrial applicability. Most of the members of the FMICS community have strong links with industry and have thus contributed to the slow but constant introduction of formal methods in the development cycle of industrial critical systems witnessed in the last decade. The WG has also addressed other readily applicable verification techniques, such as static analysis by abstract interpretation. Similarly, the whole formal development lifecycle has been addressed, for example in the 2008 FMICS workshop where considerable attention was paid to the recent diffusion of Model Driven Development in industry.

In 2008, issue number 75 of the ERCIM News hosted a joint special session edited by Pedro Merino, coordinator of the WG, and Erwin Schoitsch, coordinator of the DES Dependable Embedded System WG, featuring almost 30 articles, many of which reporting advances on the application of formal methods in industry.

The FMICS workshop series has always been open to contributions from outside the ERCIM community, and strong links have been maintained with other organizations, such as Formal Methods Europe. In November 2009, the FMICS workshop will be held during the FM week, a special gathering of events organized this year by the FME association.

2.      Background

Formal methods have been advocated as a means of increasing the reliability of systems, especially those which are safety or business critical, but the industrial uptake of such methods has been slow. This is due to the perceived difficulty of mathematical nature of these methods, the lack of tool support, and the lack of precedents where formal methods has been proven to be effective. It is even more difficult to develop automatic specification and verification tools due to limitations like state explosion, undecidability, etc. This working group will bring together researchers of the ERCIM consortium in order to promote the use of formal methods within industry.

The behaviour of reactive systems is largely conditioned by the interaction with events of the external environment the sequentialization of which is not predictable. The complexity of the systems' behaviour increases considerably when the timing dependencies in the execution of events are taken into account.

The above features are typical of a large class of systems including control systems, automation systems, and communication systems and results in the extreme difficulty of the verification of their correctness.

In the industrial context correctness verification is usually performed by means of testing; the system is provided with input sequences drawn from a proper "coverage set" and its resulting behaviour is observed.

Due to the multiplicity of possibilities both for inputs to a system and originating from more and more use of parallelism and concurrency this approach turns out to be very costly and in any case it does not allow for the exhaustive verification of the correctness of the system. It allows only to detect errors which take place during the execution sequences used for the test.

In the last decade several theories have been developed which aim at coping with the problem of systems correctness by means of formal methodologies for the specification, design and verification of systems. These theories have been extended in order to deal with time, probability and stochastic aspects of behaviours.

Also real-time models where time is a dense quantity and verification can be done algorithmically (automatically) has been developed.

More recently, international standards for safety recommend the use of such methodologies, especially for critical systems.

Nevertheless, the use of formal methods in the industry is still quite limited. Apparently, major reasons for that are the notational difficulty of most formal methods available nowdays and the lack of integration between them. Notational complexity is often a deterrent to the use of formal methods stronger than the advantages of such methods. This is reinforced by the lack of models which support all the activities of system development:

  1. requirements specification
  2. validation of the specification
  3. design
  4. verification of the final product against the requirements
For each of the above activities different techniques have been developed independently. They are usually not at all integrated, neither compatible and quite often they have been tried only on toy-examples, bringing to results which are rather difficult to compare. Finally, most of the automatic tools developed for supporting the use of formal methods lack of industrial strength and so turn out to be unpractical when used in the industrial context.

3.      Objectives

The main objectives of the WG are:
  1. To bring together scientists mainly of, but not only of, institutions within ERCIM, who are active in the field of formal methods and are willing to exchange their experience in the industrial usage of formal methods.
  2. To coordinate efforts in the transfer of the formal methods technology and knowledge to the industry.
  3. To promote research and development for the improvement of formal methods and tools with respect to their usage in the industry.
The above objectives will be met by means of:
  1. Workshops where the participation of industrial professionals will be solicited.
  2. Development projects with industrial partners.
  3. Research projects and researchers mobility.

4.      Scientific Activities

  1. First International Workshop on Formal Methods for Industrial Critical Systems
    St. Hugh's College, Oxford (UK), March 19, 1996

  2. Special issue of the journal "Formal Methods in System Design"
    (Vol. 12, Nr. 2, March 1998)

  3. Second International Workshop on Formal Methods for Industrial Critical Systems
    Cesena (Italy), July 4-5, 1997

  4. Special issue of the journal "Formal Aspects of Computing"
    (Vol. 10, Nr. 4, 1998)

  5. Third International Workshop on Formal Methods for Industrial Critical Systems
    Amsterdam (The Netherlands), May 25-26, 1998

  6. Special issue of the journal "Formal Aspects of Computing"
    (Vol. 10, Nr. 5-6, 1998)

  7. Fourth International Workshop on Formal Methods for Industrial Critical Systems
    Trento (Italy), July 11-12, 1999

  8. Special issue of the journal on "Science of Computer Programming"
    (Vol. 36, Issue 1, January 2000)

  9. Fifth International Workshop on Formal Methods for Industrial Critical Systems
    Berlin (Germany), April 3-4, 2000

  10. Special issue of the journal "Formal Methods in System Design"
    (Vol. 19, Nr. 2, September 2001)

  11. Sixth International Workshop on Formal Methods for Industrial Critical Systems
    Paris (France), 16-17 July 2001

  12. Seventh International Workshop on Formal Methods for Industrial Critical Systems
    Málaga (Spain), 12-13 July 2002

  13. Special issue of the journal on "Science of Computer Programming"
    (Vol. 46, Nr. 3, March 2003).

  14. Eight International Workshop on Formal Methods for Industrial Critical Systems
    Trondheim (Norway), 5-7 July 2003

  15. Special issue of the journal "Software Tools for Technology Transfer"
    (Vol. 5, Nr. 2-3, March 2004)

  16. Ninth International Workshop on Formal Methods for Industrial Critical Systems
    Linz (Austria), 20-21 September 2004

  17. Tenth International Workshop on Formal Methods for Industrial Critical Systems
    Lisbon (Portugal), 5-6 September 2005

  18. Eleventh International Workshop on Formal Methods for Industrial Critical Systems
    Bonn (Germany), 26-27 August 2006

  19. Special issue of the journal "Formal Methods in System Design"
    (Vol. 30, Nr. 3, June 2007)

  20. Twelth International Workshop on Formal Methods for Industrial Critical Systems
    Berlin (Germany), 1-2 July 2007 (LNCS Proceedings)

  21. European project EC-MOAN
    2007-2009

  22. Thirteenth International Workshop on Formal Methods for Industrial Critical Systems
    L'Aquila (Italy), 15-16 September 2008 (LNCS Proceedings)

  23. Fourteenth International Workshop on Formal Methods for Industrial Critical Systems
    Eindhoven (The Netherlands), 2-3 November 2009 (LNCS Proceedings)

  24. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 11, Nr. 5, Nov. 2009)

  25. Fifteenth International Workshop on Formal Methods for Industrial Critical Systems
    Antwerp (Belgium), 20-21 September 2010 (LNCS Proceedings)

  26. Special issue of the journal "Science of Computer Programming" (Vol. 76, Nr. 2, Feb. 2011)

  27. Sixtenth International Workshop on Formal Methods for Industrial Critical Systems
    Trento (Italy), 29-30 August 2011

5.      Official ERCIM Documents about FMICS

6.      Contacts

As of November 1st, 2011, the FMICS Working Group is being chaired by:
 
Radu Mateescu
INRIA Grenoble - Rhône-Alpes
Inovallee - 655, avenue de l'Europe
Montbonnot
F-38334 Saint Ismier Cedex
FRANCE
tel: +33 (0)4 76 61 54 86
fax: +33 (0)4 76 61 52 52
e-mail: Radu.Mateescu@inria.fr

The FMICS Chair is assisted by the FMICS Board, the members of which are:

The former FMICS Chairs are:

7.      Institutions and Participants

The FMICS Working Group is currently composed by researchers of the following ERCIM institutions and researchers:

STFC (formerly CCLRC)
Alvaro E. Arenas
Juan Bicarregui
David Duce
CNR
Tommaso Bolognesi
Giorgio Faconti
Stefania Gnesi
Diego Latella
Fabio Martinelli
Mieke Massink
Luca Simoncini
Maurice ter Beek
CRCIM
Lubos Brim
Antonin Kucera
Jitka Stribrna
CWI
Stefan Blom
Jens Calame

Mohammad Dashti
Wan Fokkink
Jan Friso Groote
Natalia Ioustinova
Jan Willem Klop
Bert Lisser
Simona Orzan
Jun Pang
Jaco van de Pol
Yanjing Wang
Michael Weber
SARIT
FNRS & FWO
Fraunhofer Institute for Software and Systems Engineering (ISST)
Jakob Rehof
Fraunhofer Gesellschaft
Reinhard Budde
Jan de Meer
Monika Müllerburg
Axel Poigné
Axel Rennoch
Ina Schieferdecker
Karl-Heinz Sylla
INRIA
Robert De Simone
Hubert Garavel
Alain Girault
Claude Jard
Thierry Jéron
Jean-Marc Jézéquel
Gérard Le Lann
Radu Mateescu
Vlad Rusu
Éric Rutten
Jean-Pierre Talpin
SparCIM
SICS
Lars-åke Fredlund
MTA SZTAKI - Computer and Automation Research Institute, Hungarian Academy of Sciences
Tamas Bartha

Beyond ERCIM, the following institutions/researchers also participate to the FMICS Working Group:

CNRS / LRI
Marie-Claude Gaudel
Embedded Systems Institute
Jan Tretmans
ENEL / SRI
Edoardo Corsetti
ENS Lyon
Pierre Lescanne
FBK-irst, Embedded Systems Unit (ITC / IRST)
Alessandro Cimatti
Marco Pistore
Marco Roveri
Nokia Research Center (Finland)
Sari Leppänen (formerly Sari Männynsalo)
LIAFA - Université Paris 7
Mihaela Sighireanu
Agathe Merceron
LRDE / EPITA
Sylvain Peyronnet
Equipe de Logique Mathématique - Université Paris 7
Richard Lassaigne
OBLOG Software S.A.
Paulo J. F. Carreira
ONERA / CERT
Marielle Doche
Technische Universität Berlin
Adam Wolisz
Università di Bologna
Marco Bernardo
Roberto Gorrieri
University of Edinburg
Stephen Gilmore
Technische Universiteit Eindhoven
Dennis Dams Anton Wijs
Università di Firenze
Rocco De Nicola
Alessandro Fantechi
Rijksuniversiteit Groningen
Wim H. Hesselink
McMaster University - Hamilton
Mark Lawford
Katholieke Universiteit Nijmegen
Judi Romijn
Technische Universität München - Institut für Informatik
Jan Jürjens
Martin Leucker
Università di Pisa
Carlo Montangero
University of Southampton
Ulrich Ultes-Nitsche
Universiteit Twente
Pedro R. D'Argenio
Taolue Chen
Holger Hermanns
Joost-Pieter Katoen
Tomas Krilavicius
Carnegie-Mellon University
Miroslav Velev
Université de Poitiers
Yamine Ait Ameur
Johannes Kepler Universität Linz - Institute for Formal Models and Verification
Armin Biere
Universität Dortmund - Informatik Lehrstuhl 5
Bernhard Steffen
Universität Potsdam - Service and Software Engineering
Tiziana Margaria
University of Konstanz
Stefan Leue
Université du Luxembourg
Sjouke Mauw
Radboud University Nijmegen / LaQuSo
Marko van Eekelen
Centre National d'Etudes Spatiales and IRIT
Sandra Steere (Sandra Basnyat)
Emppoo
Guillaume Fortaine
University of Naples Federico II and Ansaldo STS Italy
Francesco Flammini
Oak Ridge National Laboratory
Andrew S. Loebl
University of Parma, Italy - Applied Formal Methods Laboratory
Roberto Bagnara
University of Southern Denmark - Department of Mathematics and Computer Science
Peter Schneider-Kamp
Bogazici University, Istanbul, Turkey - Department of Computer Engineering
Alper Sen
National University of Singapore - School of Computing
Sun Jun
Manchester University
Manuela Bujorianu
University of Portsmouth
Benjamin Aziz
INTECS
Silvia Mazzini
Aarhus University / Aarhus School of Engineering
Peter Gorm Larsen
University of Liverpool - Department of Computer Science
Michael Fisher
Åbo Akademi University
Maryam Kamali
Imperial College
Alastair Donaldson

If you are interested in joining the FMICS Working Group, please send an e-mail to Hubert.Garavel@inria.fr (please indicate your official e-mail address and the URL of your Web page, if any).