7th International Workshop on
Formal Methods for Industrial Critical Systems
FMICS 02
Málaga (Spain), 12-13 July 2002

Friday 12 July 2002

8.30 - 9.00

Registration

9.00

Opening of Workshop

9.00 - 10.00

Invited Presentation: Andreas Podelski (Max-Planck Institut für Informatik, Germany)
Abstraction for Software Model-Checking

SESSION 1

ABSTRACTION AND MODEL-CHECKING - Chair: Hubert Garavel (INRIA Rhône-Alpes, France)

10.00 - 10.30

M. Bourahla (University of Biskra, Algeria), M. Benmohamed (University of Constantine, Algeria)

Predicate Abstraction and Refinement for Model Checking VHDL State Machines

10.30 - 11.00

M. del Mar Gallardo, J. Martinez, P. Merino, E. Pimentel (University of Málaga, Spain)

A Tool for Abstraction in Model Checking

11.00 - 11.30

Coffee Break

SESSION 2

TESTING - Chair: Rance Cleaveland (SUNY, New York, USA)

11.30 - 12.00

D. Lugato, C. Bigot, Y. Valot (CEA Saclay, France)

Validation and Automatic Test Generation on UML Models: The AGATHA Approach

12.00 - 12.30

J.C. Burguillo, M. Llamas, M.J. Fernández (University of Vigo, Spain), T. Robles (Polytechnical University of Madrid, Spain)

Heuristic-driven Techniques for Test Case Selection

12.30 - 13.00

T. Margaria (METAFrame Technologies GmbH, Germany), B. Steffen (University of Dortmund, Germany)

Scalable System-level CTI Testing through Lightweight Coarse-grained Coordination

13.00 - 15.00

Lunch

15.00 - 16.00

Invited Presentation: Andrew D. Gordon (Microsoft Research, Cambridge, UK)
Authenticity Types for Cryptographic Protocols

SESSION 3

INDUSTRIAL CASE STUDIES I - Chair: Holger Hermanns (University of Twente, NL)

16.00 - 16.30

N. Lopez, M. Simonot, V. Donzeau-Gouge (CNAM, Paris, France)
A Methodological Process for the Design of a Large System: Two Industrial Case-Studies

16.30 - 17.00

C. Daws (CWI, Amsterdam, NL), M. Kwiatkowska, G. Norman (University of Birmingham, UK)

Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM

17.00 - 17.15

Coffee Break

17.15 - 18.00

TOOL DEMOS

21.00 -

Workshop Dinner

Saturday 13 July 2002

9.00 - 10.00

Invited Presentation: Wang Yi (Uppsala University, Sweden)
Synthesis of Verified Real Time Software

SESSION 4

INDUSTRIAL CASE STUDIES II - Chair: Wan Fokkink (CWI, Amsterdam, NL)

10.00 - 10.30

V. Valero, F.L. Pelayo, F. Cuartero, D. Cazorla (University of Castilla-La Mancha, Spain)

Specification and Analysis of the MPEG-2 Video Encoder with Timed-Arc Petri Nets

10.30 - 11.00

S. Boldo, M. Daumas (Ecole Normale Supérieure de Lyon, France)

Properties of the Subtraction Valid for any Floating Point System

11:00 - 11.30

Coffee Break

SESSION 5

MODEL CHECKING - Chair: Stefania Gnesi (IEI-CNR, Pisa, Italy)

11.30 - 12.00

X. Thirioux (IRIT-LIMA, Toulouse, France)

Simple and Efficient Translation from LTL Formulas to Buchi Automata

12.00 - 12.30

A. Biere, C. Artho, V. Schuppan (ETH Zürich, Switzerland)

Liveness Checking as Safety Checking

12.30 - 13.00

H. Hansen (Tempere Univ. of Technology, Finland), W. Penczek (Institute of Computer Science, Poland), A. Valmari

Stuttering-Insensitive Automata for On-the-Fly Detection of Livelock Properties

13.00 - 15.00

Lunch

15.00 - 15.30

A.Valmari, H. Virtanen, A. Puhakka (Tempere University of Technology, Finland)

Context-Sensitive Visibility

15.30 - 17.00

FMICS Working Group Meeting

17.00

Closing of Workshop