4th ProCoS Working Group Meeting

11-13 March 1996
Oldenburg, Germany

PROGRAMME

• real-time and hybrid systems,
• linking different formal methods,
• mechanical support of these methods.

The highlight was a presentation of three German projects on formal methods for correct systems.

Sunday, 10 March:

Arrival of participants

Monday, 11 March:

 9.00  OPENING

morning: Real-Time Systems

 9.15  Zhou Chaochen, DTU Lyngby, Denmark:
       Duration Calculi -- An Overview  (30 min)
 
10.00  Martin Fränzle, Uni Kiel:
       Synthesizing Controllers from Duration Calculus Specifications
       (45 min)
 
11.00  COFFEE
 
11.30  Michael Hansen, DTU Lyngby, Denmark:
       Super Dense Chop in Duration Calculus  (30 min)
 
12.15  Henning Dierks, Uni Oldenburg:
       Production Cell viewed as Real-Time System  (30 min)
 
13.00  LUNCH
 
afternoon: Action and Mixed System

14.30  Kaisa Sere, Abo Akademi, Finland:
       Modular Action Systems  (30 min)
 
15.15  Emil Sekerinski, Abo Akademi, Finland:
       Refining Untimed to Timed Specifications  (30 min)
 
16.00  COFFEE
 
Special Lecture
 
16.30  Tony Hoare, Oxford University:
       How Did Software Get So Reliable Without Proof ?
 
18.00  RECEPTION
 
Tuesday, 12 March:

morning: Mixed Systems, cont'd
 
 9.00  Stephan Kleuker, Uni Oldenburg:
       Incremental Development of Correct Specifications for
       Distributed  Systems (30 min)
 
morning: Hardware Design

 9.40  Augusto Sampaio, Recife, Brazil:
       Hardware/Software Codesign: The PISH Project (30 min)
 
10.20  Andrew Bailey, Oxford Univ:
       VLSI Programming (30 min)
 
11.00  COFFEE
 
morning: Mechanic Support for Linking Theories

11.30  Paul Curzon, Cambridge Univ, England:
       Checking Proofs from Linked Tools  (30 min)
 
12.15  Job Zwiers, Uni Twente, The Netherlands:
       Formal Methods applied to the
       Nieuwe Waterweg Dam  (30 min)
 
13.00  LUNCH
 
afternoon: ProCoS Tutorial

14.30  Markus Müller-Olm, Ernst-Rüdiger Olderog, Anders Ravn:
       The ProCoS Approach to the Design of Real-Time Systems:
       Linking Different Formalisms

16.00  COFFEE

late afternoon

17.00  Jonathan Bowen, Reading Univ, England:
       ProCoS-WG business meeting

evening

19.00  SOCIAL DINNER


Wednesday, 13 March:

all day: presentations of the projects ESPRESS, KORSYS and UNIFORM

Project ESPRESS

 8.30  Stefan J&aulm;hnichen, TU Berlin:
       The ESPRESS Project - An Overview  (15 min)
 
 9.00  Matthias Weber, TU Berlin:
       Integrating Mathematical Techniques in the
       Development of Embedded Control Systems  (20 min)
 
 9.30  Wolfgang Grieskamp, TU Berlin:
       Proposal for a Language Integrating Z and Statecharts (20 min)
 
10.00  Robert Geisler, TU Berlin:
       Case Study: A Traffic Light Control System  (20 min)
 
10.30  COFFEE
 
Project KORSYS

11.00  Gerd Venzl, Siemens Munich:
       The KorSys Project - Overview, Goals, and Topics (20 Min)

11.30  Thomas Filkorn, Siemens Munich:
       Model-Checking Techniques (40 Min)
 
12.15  Werner Damm, Uni Oldenburg:
       The KorSys Method for Embedded Systems (40 Min)
 
13:00  LUNCH
 
Project UNIFORM

14.00  Bernd Krieg-Brückner, Uni Bremen:
       The UniForM-Project - An Overview (20 min)
 
14.30  Clemens Fischer, Uni Oldenburg:
       Combining MIX and Z  (20 min)
 
15.00  Burkhart Wolff, Uni Bremen:
       Encoding transformations in higher order logic  (20 min)
 
15.30  Bernd Krieg-Brückner, Uni Bremen:
       The UniForM Workbench  (20 min)
 
16.00  CLOSING