Working Group on Formal Methods for Industrial Critical Systems

Fifth International Workshop on Formal Methods for Industrial Critical Systems

Berlin (Germany)

April 3-4, 2000


(with access to the individual contributions)

Monday 3rd April, 2000

8:30h. - 9:30h.: Registration

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

Tuesday 4th April, 2000

Invited talk (chair: H. Garavel):
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


Last modified: Monday, 17-Apr-2000 16:40:00 MET DST, Axel Rennoch

Back to the ERCIM FMICS Home Page