Formal Methods Europe Symposium 1997

Programme

The Symposium will take place from Wednesday, 17th September to Friday, 19th September. Each day will have three Sessions: In session one three contributed papers will be presented in a single track. Session 2 and 3 will be held in two parallel tracks. If you want to register for this symposium you can use this online registration form.

Wednesday, 17th September

Opening (9:00 - 9:30)

Invited Lecture (9:30 - 10:30)

• Hermann Kopetz, Technical University of Vienna:
  The Design of Time-Triggered Real-Time Systems

Session 1 (11:00 - 12:30)

• Stuart O. Anderson, Konstantinous Tourlas, Univ. of Edinburgh:
  Diagrams and Programming Languages for Programmable Controllers
• Henning Dierks, Cheryl Dietz, Univ. of Oldenburg:
  Graphical Specification and Reasoning: Case Study Generalized Railroad Crossing
• Mauro Larosa, Gianna Reggio, Universita di Genova:
  A Graphic Notation for Formal Specifications of Dynamic Systems

Session 2a (14:00 - 15:00)

• Graeme Smith, Tech. Univ. Berlin:
  A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems
• Anna Mikhajlova, Emil Sekerinski, Abo Akademi University:
  Class Refinement and Interface Refinement in Object-Oriented Programs

Session 2b (14:00 - 15:00)

• Stephan Kleuker, Univ. of Oldenburg:
  Formalizing requirements for distributed systems with trace diagrams
• Geralf Einert, Franz Huber, Bernhard Schatz, Tech. Univ. Muenchen:
  Consistent Graphical Specification of Distributed Systems

Session 3a (15:30 - 17:00)

• K. Lano, A. Sanchez, Imperial College:
  Design of Real-time Control Systems for Event-driven Operations
• Hans Fleischhack, Josef Tapken, Univ. of Oldenburg:
  An M-Net Semantics for Real-Time Extension of muSDL
• M. Broy, R. Grosu, C. Klein, Tech. Univ. Munchen:
  Reconciling Real-Time with Asynchronous Message Passing

Session 3b (15:30 - 17:00)

• Martin Schoenhoff, Mojgan Kowsari, Tech. University of Zurich and Tech. Univ. Braunschweig:
  Specifying the Remote Controlling of Values in an Explosion Test Environment
• Lionel Devauchelle, Peter Gorm Larsen, Henrik Voss, Aerospatiale Espace et Defense and IFAD:
  PICGAL: Practical use of Formal Specification to Develop a Complex Critical System

Thursday, 18th September

Invited Lecture (9:00 - 10:00)

• Loe Fejis, Philips Research Laboratories, The Netherlands:
  Tutorial and experience report on COLD and SPRINT

Session 1 (10:30 - 12:00)

• William D. Young, William R. Bevier, Computational Logic Inc.:
  Mathematical Modeling and Analysis of an External Memory Manager
• Paul Mukherjee, Univ. Leeds:
  Automatic Translation of VDM-SL specifications into Gofer
• Sten Agerholm, Jacob Frost, IFAD and Technical University of Denmark:
  Towards an Integrated CASE and Theorem Proving Tool for VDM-SL

Session 2a (13:30 - 14:30)

• J. Fiadeiro, A. Lopes, K. Lano, J. Bicarregui, University of Lisbon and Imperial College:
  Specification of Required Non-determinism
• H. Tej, B. Wolff, Univ. Bremen:
  A Corrected Failure-Divergence Model for CSP in Isabelle/HOL

Session 2b (13:30 - 14:30)

• Bernhard K. Aichernig, Peter Gorm Larsen, Technical University Graz and IFAD:
  A Proof Obligation Generator for VDM-SL
• Marc Mehdi Ayadi, Dominique Bolignano, Universite Paris IX Dauphine and Dyade:
  Verification of Cryptographic Protocols: an Experiment

Session 3a (15:00 - 16:30)

• J-Cu. Gregoire, INRS-Telecommunications:
  TLA + PROMELA: Conjecture, Check, Proof. Engineering new protocols using methods and formal notations
• A. Mokkedem, Michael J. Ferguson, Robert deB Johnston, INRS-telecommunications:
  A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol
• Jeremy Martin, Sabah Jassim, Oxford University Computing Services:
  An Efficient Technique for Deadlock Analysis of Large Scale Process Networks

Session 3b (15:00 - 16:30)

• Shenwei Yu, Zhaohui Luo, Univ. of Durham:
  Implementing a Model Checker for LEGO
• A. Dold, F. W. von Henke, H. Pfeifer, H. Ruess, Univ. Ulm:
  Formal Verification of Transformations for Peephole Optimiztion

Friday, 19th September

Invited Lecture (9:00 - 10:00)

• Robin Bloomfield, Adelard, U.K.:
  Formal methods and commercial reality: recent experiences in the industrial use of formal methods

Session 1 (10:30 - 12:00)

• Richard F. Paige, Univ. of Toronto:
  A Meta-Method for Formal Method Integration
• David Hemer, Peter A. Lindsay, Univ. of Queensland:
  Reuse of verified design components
• F. S. de Boer, U. Hannemann, W.-P. de Roever, Utrecht Univ. and Christian-Albrechts-Univ. Kiel:
  A compositional proof system for shared variable concurrency

Session 2a (13:30 - 14:30)

• Pierre Michel, Virginie Wiels, ONERA-CERT:
  A framework for modular formal specification and verification
• C. Petersohn, L. Urbina, Christian-Albrechts-Univ. Kiel:
  A Timed Semantics for the STATEMATE Implementation of Statecharts

Session 2b (13:30 - 14:30)

• David W. J. Stringer-Calvert, Susan Stepney, Ian Wand, Univ. of York and Logika U.K. Ld.:
  Using PVS to Prove a Z refinement: A Case Study
• Pertti Kellomaki, Tampere Univ. of Technology:
  Verification of Reactive Systems Using DisCo and PVS

Session 3a (15:00 - 16:00)

• David Cazier, Jean-Francois Dufourd, LSIIT UR CNRS 1871:
  Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects
• Leila Silva, Augusto Sampaio, Edna Barros, Univ. Federal de Pernambuco:
  A Normal Form Reduction Strategy for Hardware/Software Partitioning

Session 3b (15:00 - 16:00)

• Eerke Boiten, Howard Bowman, John Derrick, Maarten Steen, Univ. of Kent at Canterbury:
  Viewpoint consistency in Z and LOTOS: A case study
• Michel Charpentier, ENSEEIHT:
  A UNITY composition operator for distributed programs