jETI Logo  
 

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

Home Page


Recent and Forthcoming Events (updated 06/04/14)

Table of contents

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

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

3.      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"
    5. (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

4.      Official ERCIM Documents about FMICS

5.      Contacts

Since November 2005, the FMICS Working Group is chaired by Dr. Pedro Merino (SpaRCIM):
 
Pedro Merino
Dpto. de Lenguajes y Ciencias de la Computación
ETSI Telecomunicación - ETSI Informática
Universidad de Málaga
Campus de Teatinos
29071 Málaga
SPAIN
tel: +34 (5) 213 2752
fax: +34 (5) 213 1397
e-mail: pedro@lcc.uma.es

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

The former FMICS Chairs are:

6.      Institutions and Participants

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

CLRC
Alvaro E. Arenas
Juan Bicarregui
David Duce
CNR
Tommaso Bolognesi
Giorgio Faconti
Stefania Gnesi
Diego Latella
Fabio Martinelli
Mieke Massink
Fabio Paterno
Luca Simoncini
Maurice ter Beek
CRCIM
Lubos Brim
Antonin Kucera
Jitka Stribrna
CWI
Bahareh Badban
Stefan Blom
Wan Fokkink
Jan Friso Groote
Natalia Ioustinova
Jan Willem Klop
Izak van Langevelde
Bert Lisser
Sjouke Mauw
Simona Orzan
Jun Pang
Jaco van de Pol
Miguel Valero Espada
SARIT
FNRS & FWO
GMD
Reinhard Budde
Jan de Meer
Monika Müllerburg
Axel Poigné
Axel Rennoch
Ina Schieferdecker
Karl-Heinz Sylla
Adam Wolisz
INRIA
Robert De Simone
Hubert Garavel
Alain Girault
Claude Jard
Thierry Jéron
Jean-Marc Jézéquel
Christophe Joubert
Gérard Le Lann
Radu Mateescu
Vlad Rusu
Éric Rutten
Jean-Pierre Talpin
SparCIM
Maria-del-Mar Gallardo
Pedro Merino Gómez
SICS
Lars-ĺke Fredlund

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

CETIC
André Rifaut
Christophe Ponsard
Jean-François Molderez
CNRS / LRI
Marie-Claude Gaudel
ENEL / SRI
Edoardo Corsetti
ENS Lyon
Pierre Lescanne
ITC / IRST
Alessandro Cimatti
Marco Pistore
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
Technische Universiteit Eindhoven
Dennis Dams
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
Holger Hermanns
Joost-Pieter Katoen
Tomas Krilavicius
Jan Tretmans
Carnegie-Mellon University
Miroslav Velev
Université de Poitiers
Yamine Ait Ameur
Johannes Kepler Universität Linz - Institute for Formal Models and Verification
Armin Biere

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


back Back to the VASY Home Page