FMICS 2004 - Ninth International Workshop on Formal Methods for Industrial Critical Systems

by Juan Bicarregui, Andrew Butterfield and Alvao Arenas

The Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 04) was held in Linz, Austria, during September 20-21, as a co-located event of the 19th IEEE Conference on Automated Software Engineering. The workshop series promotes the use of formal methods for industrial applications by supporting research in this area and by serving as a forum for the exchange of ideas between researchers and practitioners, in both industry and academia.

This workshop, organised by the ERCIM Working Group on Formal Methods for Industrial Critical Systems and CCLRC Rutherford Appleton Laboratory, was attended by 35 participants from academia and industry from 16 countries. The two keynote speakers gave interesting and stimulating presentations. Jeremy Dick from Telelogic spoke on linking formal methods to formal requirements describing how existing tools for supporting requirements traceability could be adapted to work with formal specification and refinement documents. Cedric Fournet of Microsoft Research spoke on the verification of the security of XML-based web-services and described how the 'applied' pi-calculus was used to analyse the safety of security policies, work which has contributed to recent revisions of Microsoft code. FMICS would like to thank both invited speakers for their relevant and highly informative contributions to the success of the workshop.

Seventeen submitted papers were presented with authors from 17 countries spanning formal methodologies as diverse as state-charts, model-checking, mixed intuitionistic logic and Boolean equation systems; and applications ranging from operating systems, network services, communications protocols and middleware behaviour, to flight guidance.

The best paper award supported by the European Association of Software Science and Technology (EASST) was awarded to Martin Fränzle and Christian Herde for their paper on proof engines for bounded model checking of hybrid systems.

Other papers presented included Object Oriented concepts identification from formal B specifications; an Abstract Interpretation Toolkit for _CRL; Early Verification and Validation of Critical Systems; and Model Checking Flight Guidance Systems: from Synchrony to Asynchrony, among others

The proceedings of the workshop are published as a technical reports of the Johannes Kepler University and will appear in Electronic Notes in Theoretical Computer Science. Selected papers will be invited for publication in an special issue of Formal Methods in System Design.

The organisers wish to thank FME and the i-Trust Working Group for sponsorship for the invited speakers. Participants enjoyed a good Austrian dinner courtesy of ERCIM.

Links:
Ninth International Workshop on Formal Methods for Industrial Critical Systems: http://www.fmics04.clrc.ac.uk/

ERCIM Working Group on Formal Methods for Industrial Critical Systems:
http://www.inrialpes.fr/vasy/fmics/

Please contact:
Juan Bicarregui, CCLRC, UK
Tel: + 44 1235 445710
E-mail: J.C.Bicarregui@rl.ac.uk