Working Group on Formal Methods for Industrial Critical Systems

Seventh International Workshop on Formal Methods for Industrial Critical Systems (FMICS 02)

University of Málaga (Spain)

July 12-13, 2002

Colocated with the 29th ICALP conference


  • Andrew D. Gordon (Microsoft Research, Cambridge, UK)

    Authenticity Types for Cryptographic Protocols

    based on joint work with Alan Jeffrey, DePaul University (Chicago, IL, USA)

    Cryptographic protocols are essential for the security of many critical networking applications, such as authenticating various financial transactions. Moreover, many new consumer-to-business and business-to-business protocols are being proposed and need cryptographic protection. It is famously hard to specify and verify such protocols, even if we assume that the underlying cryptographic algorithms cannot be cryptanalysed. My invited talk describes a new approach to specifying and verifying authenticity properties of security protocols, based on a typed process algebra. The theory has been developed in a series of papers with Alan Jeffrey. Our approach requires little human effort per protocol, puts no bound on the size of the opponent attacking the protocol, and requires no state space enumeration. Moreover, the types for protocol data provide Some intuitive explanation of how the protocol works. My talk explains the basic ideas by example, states our main results, and outlines our plans for applications of this technology.

      A.D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. In 15th IEEE Computer Security Foundations Workshop (CSFW 2002), Cape Breton, June 24-26, 2002. IEEE Computer Society.

      A.D. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW 2001), pages 145-159, Cape Breton, June 11-13, 2001. IEEE Computer Society. A journal version is to appear in the Journal of Computer Security.

      A.D. Gordon and A. Jeffrey. Typing correspondence assertions for communication protocols. In Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001), Elsevier ENTCS 45, 2001. A journal version is to appear in Theoretical Computer Science.

  • Andreas Podelski (Max-Planck-Institut für Informatik, Germany)

    Abstraction for Software Model Checking

    based on joint work with Tom Ball and Sriram Rajamani (Microsoft Research, Redmond WA, USA), and Andrei Rybalchenko (Max-Planck-Institut, Germany)

    A program with variables over unbounded data domains (e.g. integers) generates an infinite-state transition system. Thus, one approach to extend model checking to software works by mapping an infinite-state transition system to a finite one. We explain the limitations of that approach and show how one can go beyond. We present a whole spectrum of abstractions with different precision/cost trade-off's. In order to automatize software model checking, we combine the automated process of abstraction with an automated process to make the abstraction more and more precise (namely until the property can be proven in the abstract). We present new ideas on parametrizing such an `abstraction refinement' process.

      T. Ball, A. Podelski, and S. Rajamani. Relative Completeness of Abstraction Refinement for Software Model Checking. In Proceedings of TACAS 2002, LNCS 2280, pages 158-172.

  • Wang Yi (Uppsala University, Sweden)

    Synthesis of Verified Real Time Software

    In this talk. I will present a unified model for timed systems to bridge scheduling, model checking and code synthesis. The technical contributions include a general notion of schedulability for automata and efficient algorithms for schedulability checking. TIMES is a tool developed based on these recent results and our past experience in developing the UPPAAL tool. It is designed for synthesis of verified software guaranteeing timing constraints. This talk will review recent development on TIMES and published results from papers.

      Elena Fersman, Paul Pettersson, and Wang Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. Proceedings of TACAS 2002, LNCS 2280, pages 67-82

      Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. Times - A Tool for Modelling and Implementation of Embedded Systems. Proceedings of TACAS 2002, LNCS 2280, pages 460-464.


  • Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM
    C. Daws, M. Kwiatkowska and G. Norman
  • A Methodological Process for the Design of a Large System: Two Industrial Case-Studies
    N. Lopez, M. Simonot, V. Donzeau-Gouge
  • Predicate Abstraction and Refinement for Model Checking VHDL State Machines
    Mustapha Bourahla and Mohamed Benmohamed
  • Simple and Efficient Translation from LTL Formulas to Buchi Automata
    Xavier Thirioux
  • Context-Sensitive Visibility
    Antti Valmari, Heikki Virtanen and Antti Puhakka
  • Heuristic-driven Techniques for Test Case Selection
    J.C. Burguillo, M. Llamas, M.J. Fernández, T. Robles.
  • Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties
    Henri Hansen, Wojciech Penczek, Antti Valmari
  • Liveness Checking as Safety Checking
    Armin Biere, Cyrille Artho, Viktor Schuppan
  • A Tool for Abstraction in Model Checking
    Maria del Mar Gallardo, Jesus Martinez, Pedro Merino, Ernesto Pimentel
  • Scalable System-level CTI Testing through Lightweight Coarse-grained Coordination
    B. Steffen, T. Margaria, O.Niese
  • Validation and Automatic Test Generation on UML Models: the AGATHA approach
    David Lugato, Celine Bigot, Yannick Valot
  • Properties of the Subtraction Valid for any Floating Point System
    Sylvie Boldo, Marc Daumas
  • Specification and Analysis of the MPEG-2 Video Encoder with Timed-Arc Petri Nets
    Valentin Valero, Fernando L. Pelayo, Fernando Cuartero, Diego Cazorla


ERCIM FMICS Home Page, University of Málaga Home Page

Last modified: 2011/11/24 14:55:35, Hubert Garavel