(with access to the individual contributions)
| 9:30h. - 9:40h.: | Opening |
Invited talk (chair: S. Gnesi):
| 09:40h. |
From Dining Philosphers to Dining Cryptographers G. Karjoth (IBM Zurich, CH) |
Session 1: Applications (chair: S. Gnesi)
| 10:30h. | A B Model for Ensuring Soundness of a Large Subset of the Java Card Virtual Machine A. Requet (Gemplus Research Lab, Gemenos, F) |
| 11:00h. | Applying Formal Methods to Industrial Cases: The Language Approach (The Production-Cell and Mode-Automata)
F. Maraninchi, Y. Rémond (VERIMAG Gieres, F) |
| 11:30h. | Session summary |
11:35h. - 12:00h.: Coffee break
Session 2: Verification (chair: D. Latella)
| 12:00h. | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
R. Mateescu (INRIA St. Martin, F), M. Sighireanu (Uni Paris 7, F) |
| 12:30h. | Verification in the Codesign process by means of LOTOS based model-checking
F. Baray, P. Wodey (Blaise Pascal Uni Clermont Ferrand II, F) |
| 12:50h. | Verification of Erlang Programs: Factoring out the Side-effect-free Fragment
D. Gurov, G. Chugunov (SICS Kista, S) |
| 13:10h. | Session summary |
13:20h. - 14:30h.: Lunch
Session 3: Testing & Software development (chair: J. Tretmans)
| 14:30h. | Specificaton-based Testing of Synchronous Software
L. du Bousquet, F. Ouabdesselam, I. Parissis, J.-L. Richier, N. Zuanon (LSR-IMAG St. Martin d'Heres, F) |
| 15:00h. | Formalization and Testing of Reference Point Facets
I. Schieferdecker, M. Li, A. Rennoch (GMD Fokus Berlin, D) |
| 15:30h. | Towards a Mechanised Software Development Method
B. Wu, L.M. Lai, D.R.W. Holton (Uni Bradford, UK) |
| 15:50h. | Integrating formal methods into the development cycle of a safety-critical embedded software system
P. Bertoli, A. Cimatti, P. Traverso (IRST Trento, I) |
| 16:10h. | Session summary |
16:20h. - 16:50h.: Coffee break
Session 4: MSC / SDL (chair: I. Schieferdecker)
| 16:50h. | Conditions for synthesis of communicating automata from HMSCs
L. Helouet, C. Jard (IRISA/CNRS Rennes, F) |
| 17:20h. | A Practical Method to Integrate Abstractions into SDL and MSC based Tools
M.M. Gallardo, P. Merino (Uni Malaga, E) |
| 17:40h. | Experiences with Tool development of SDL in Combination with ASN.1 for Communication Protocol Applications R. Schröder, M. v. Löwis of Menar (Humboldt Uni Berlin, D) |
| 18:00h. | Session summary |
18:10h.: End of 1st day
20:00h.: Workshop dinner
| 09:00h. | Performance and reliability model checking and model construction
H. Hermanns (University of Twente, NL) |
Session 5: Modelling (chair: H. Garavel)
| 09:50h. | Modeling and Verifying a Temperature Control System using Hybrid Action System
R.J. Back, C. Cerschi (TUCS Turku, FI) |
| 10:20h. | Modelling and Analysing the Railroad Crossing in a Modular Way
D. Beyer, C. Lewerentz, H. Rust (TU Cottbus, D) |
| 10:40h. | A Formal Specification and Verification of a Safety Critical Control System
S. Gnesi, D. Latella, G. Lenzini (CNR Pisa, I), C. Abbaneo, A. Amendola and P. Marmo (ASF Genova/Napoli, I) |
| 11:00h. | Session summary |
11:10h. - 11:40h.: Coffee break
Session 6: Case Studies (chair: U. Ultes-Nitsche)
| 11:40h. | A Case Study in Formal Methods: Specification and Validation of the OM/RR Protocol
T. Willemse (Eindhoven Uni, NL), J. Tretmans (Uni Twente, NL), A. Klomp (CMG Den Haag, NL) |
| 12:10h. | Automatically Verifying an Object-Oriented Specification of the Steam-Boiler System
P. Carreira and M. Costa (OBLOG Software Lisboa, P) |
| 12:40h. | Cooperative Information Systems Modelling and Validation Using the Co-nets Approach: The Chessmen Making Shop Case Study
N. Aoumeur, G. Saake (Uni Magdeburg, D) |
| 13:00h. | Session summary |
| 13:10h. - 13:15h.: | Closing |
13:15h. - 14:00h.: Lunch
14:00h. - 15:00h.: FMICS working group meeting
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Back to the ERCIM FMICS Home Page