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


Home Page


Recent and Forthcoming Events (updated 2024/10/28)

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), Radu Mateescu (INRIA), and Tiziana Margaria (LERO), 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 was 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. FMICS 1996: 1st 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. FMICS 1997: 2nd 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. FMICS 1998: 3rd 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. FMICS 1999: 4th 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. FMICS 2000: 5th 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. FMICS 2001: 6th International Workshop on Formal Methods for Industrial Critical Systems
    Paris (France), 16-17 July 2001

  12. FMICS 2002: 7th 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. FMICS 2003: 8th 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. FMICS 2004: 9th International Workshop on Formal Methods for Industrial Critical Systems
    Linz (Austria), 20-21 September 2004

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

  18. FMICS 2006: 11th International Workshop on Formal Methods for Industrial Critical Systems
    Bonn (Germany), 26-27 August 2006 (LNCS Proceedings)

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

  20. FMICS 2007: 12th 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. FMICS 2008: 13th International Workshop on Formal Methods for Industrial Critical Systems
    L'Aquila (Italy), 15-16 September 2008 (LNCS Proceedings)

  23. FMICS 2009: 14th 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. FMICS 2010: 15th 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. FMICS 2011: 16th International Workshop on Formal Methods for Industrial Critical Systems
    Trento (Italy), 29-30 August 2011 (LNCS Proceedings)

  28. FMICS 2012: 17th International Workshop on Formal Methods for Industrial Critical Systems
    Paris (France), 27-28 August 2012 (LNCS Proceedings)

  29. European project SENSATION
    2012-2015

  30. Formal Methods for Industrial Critical Systems: A Survey of Applications (Wiley, 2013)

  31. Special issue of the journal "Science of Computer Programming" (Vol. 78, Nr. 7, Jul. 2013)

  32. FMICS 2013: 18th International Workshop on Formal Methods for Industrial Critical Systems
    Madrid (Spain), 23-24 September 2013 (LNCS Proceedings)

  33. Special issue of the journal "Science of Computer Programming" (Vol. 80(A), Feb. 2014)

  34. FMICS 2014: 19th International Workshop on Formal Methods for Industrial Critical Systems
    Florence (Italy), 11-12 September 2014 (LNCS Proceedings)

  35. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 16, Nr. 6, Nov. 2014)

  36. FMICS 2015: 20th International Workshop on Formal Methods for Industrial Critical Systems
    Oslo (Norway), 22-23 June 2015 (LNCS Proceedings)

  37. Special issue of the journal "Science of Computer Programming" (Vol. 118, Mar. 2016)

  38. FMICS-AVoCS 2016: Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems
    Pisa (Italy), 26-29 September 2016 (LNCS Proceedings)

  39. FMICS-AVoCS 2017: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems
    Torino (Italy), 18-20 September 2017 (LNCS Proceedings)

  40. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 20, Nr. 4, Aug. 2018)

  41. FMICS 2018: 23rd International Conference on Formal Methods for Industrial Critical Systems
    Maynooth University (Ireland), 3-4 September 2018 (LNCS Proceedings)

  42. FMICS 2019: 24th International Conference on Formal Methods for Industrial Critical Systems
    Amsterdam (The Netherlands), 30-31 August 2019 (LNCS Proceedings)

  43. FMICS 2020: 25th International Conference on Formal Methods for Industrial Critical Systems
    Vienna (Austria), 2-3 September 2020 (LNCS Proceedings)

  44. FMICS 2021: 26th International Conference on Formal Methods for Industrial Critical Systems
    Paris (France), August 24-26, 2021 (LNCS Proceedings)

  45. FMICS 2022: 27th International Conference on Formal Methods for Industrial Critical Systems
    Warsaw (Poland), September 14-16, 2022 (LNCS Proceedings)

  46. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 24, Nr. 3, Aug. 2022)

  47. Special issue of the journal "Software Tools for Technology Transfer" (Vol. 24, Nr. 6, Dec. 2022)

  48. FMICS 2023: 28th International Conference on Formal Methods for Industrial Critical Systems
    Antwerp (Belgium), September 18-23, 2023 (LNCS Proceedings)

  49. FMICS 2024: 29th International Conference on Formal Methods for Industrial Critical Systems
    Milan (Italy), September 9-11, 2024 (LNCS Proceedings)

5.      Best Paper Awards

6.      Official ERCIM Documents about FMICS

7.      Contacts

As of October 2022, the FMICS Working Group is being chaired by:
 
Maurice ter Beek
FMT lab - ISTI-CNR
Pisa (Italy)

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

The former FMICS Chairs are:

The former FMICS Board Members are:

As of September 2020, the working group initiators are now Honorary Members of FMICS:

8.      Institutions and Participants

A legacy web page listing the FMICS members and institutions is available here. At present, participation to the FMICS working group essentially takes place by attending the annual FMICS conference.