Working Group on Formal Methods for Industrial Critical Systems

Pisa Dependable Computing Center (PDCC)



Second International Workshop on Formal Methods for Industrial Critical Systems

Cesena (Italy)

July 4-5, 1997

The First International Workshop on Formal Methods for Industrial Critical Systems took place in Oxford on March 19, 1996.

The Second International Workshop on Formal Methods for Industrial Critical Systems took place in Cesena, close to Bologna (Italy) as a Satellite Workshop to the 24th International Colloquium on Automata, Languages, and Programming, ICALP '97.

The aim of these workshops is to provide a forum mainly for, but not limited to, researchers of ERCIM sites, interested in the development and use of Formal Methods in the Industry.

In particular, these workshops should bring together scientists active in the area of formal methods and willing to exchange their experience in the industrial usage of these methods. They also aim at promoting research and development for the improvement of formal methods and tools with respect to their usage in/interest of industry.

Please notice that the workshop will be held in conjunction with the Second International Workshop on Advanced Intelligent Networks (AIN'97)

STEERING COMMITTEE

  • S. Gnesi - CNR/IEI - Pisa (IT)
  • D. Latella - CNR/CNUCE - Pisa (IT)
  • L. Simoncini - Univ. of Pisa and CNR/CNUCE - Pisa (IT)

INVITED SPEAKERS

  • E. Brinksma - University of Twente (NL)
  • U. Herzog - University of Erlangen (D)
  • R. Mazzeo - SASIB Railways (IT)
  • G. Mongardi - ANSALDO TRASPORTI (IT)

PROGRAMME COMMITTEE

  • S. Gnesi - CNR/IEI - IT (Chair)
  • J.F. Groote - CWI - NL
  • U. Nitsche - GMD - D
  • E. Madelaine - INRIA - F
  • F. Orava - SICS - S
  • B. Ritchie - CLRC - UK

ORGANIZING COMMITTEE

PROCEEDINGS

Informal participant proceedings were distributed at the workshop. A special issue of "Formal Aspects of Computing" will be published, which is dedicated to the workshop.

A report about this meeting has been published:

S. Gnesi and D. Latella. Second ERCIM International Workshop on Formal Methods for Industrial Critical Systems FMICS'97 (Cesena, Italy, July 4-5, 1997). Bulletin of the Association for Theoretical Computer Science - EATCS, number 64, February 1998.

WORKSHOP LOCATION

Palazzo Mazzini-Marinelli
Via Sacchi 3
47023 Cesena (FO)
Italy

PROGRAMME

Friday, July 4, 1997

09:10-09:20 : OPENING

09:20-10:00 : INVITED TALK
Formal Methods in the Design of a Storm Surge Barrier Control System
E. Brinksma - University of Twente

10:00-10:30 : COFFEE BREAK

10:30-11:10 : INVITED TALK
Stochastic Process Algebras for Qualitative Assurance
U. Herzog - Univ. of Erlangen-Nurnberg

11:10-11:40 :
Two Exercises with EMPA: Computing the Utilization of the CSMA/CD Protocol and Assessing the Performability of a Queueing System
M. Bernardo - Univ. of Bologna

11:40-12:10 :
Stochastic Simulation of Event Structures
J. P. Katoen - Univ. of Erlangen-Nurnberg, E. Brinksma - Univ. of Twente, D. Latella - CNR/CNUCE, R. Langerak - Univ. of Twente

12:30-14:00 : LUNCH

14.00-14.40 : INVITED TALK
Vital Processor Interlocking: A Case Study of Utilisation of Formal Methods for all the Design Phases
R. Mazzeo - SASIB Railways S.p.A.

14:40-15:10 :
A Fully Automated Approach for Proving Safety Properties in Interlocking Software using Automatic Theorem-Proving
A. Boraelv - Logikkonsult

15:10-15:50 : INVITED TALK
Formal Methods for Raylway Signalling Applications: rationale and case studies
G. Mongardi ANSALDO-Trasporti

15:50-16:10 : COFFEE BREAK

16:10-16:40 :
A Note on n Similar Parallel Processes
JF. Groote - CWI

16:40-17:10 :
Typing Confluence
U. Nestmann -INRIA, M. Steffen - Christian-Albrechts-Univ. of Kiel

17:10-17:40 :
Verification Methodology and Failure Testing in the Communication Protocol SMTP Using LOTOS
J. Gallud - Univ. of Castilla-La Mancha, M. D. Lozano - Univ. of Castilla-La Mancha, J. M. Garcia - Univ. of Murcia

17:40-18:40 : DEMOS

Saturday, July 5, 1997

09:00-09:30 :
Model checking a Mobile Telephone System
S. Gnesi - CNR/IEI, G. Ristori - Univ. of Pisa

09:30-10:00 :
CASE Support for Modular Verification of Synchronous Reactive Systems
J. Tuya - Univ. of Oviedo, C. de la Riva - Univ. of Oviedo, J. R. de Diego - Univ. of Oviedo, J. A. Corrales - Univ. of Oviedo

10.00-10.30 : COFFEE BREAK

10:30-11:00 :
Investigating the behaviour of PREMO synchronizable objects
G. Faconti, M. Massink - CNR/CNUCE

11:00-11:30 :
The SH-Verification Tool. Instruments for Verifying C0-operating systems
P. Ochsenschlaeger -GMD, J. Repp - GMD, R. Rieke - GMD, U. Nitsche - Univ. of Zurich

11:30-12:00 :
Formal Specifications for Designing User Interfaces of Air Traffic Control Applications
P. Palanque - CENA and University of Toulouse, F. Paterno' - CNR/CNUCE, R. Bastide - CENA

12:00-12:30 :
Correctness Preserving Transformations between ODP Viewpoints
C. Bernardeschi - Univ. of Pisa, A. Fantechi - Univ. of Firenze, E. Najm - ENST, A. Nimour - ENST, F. Olsen - ENST

12:30-13:00 : DISCUSSION and WORKING GROUP Meeting

Back to the ERCIM FMICS Home Page