4. FME 1997: Graz, Austria

• Stuart Anderson, Konstantinos Tourlas:
  Diagrams and Programming Languages for Programmable Controllers. 1-19
  
• Henning Dierks, Cheryl Dietz:
  Graphical Specification and Reasoning: Case Study Generalised Railroad Crossing. 20-39
  
• Gianna Reggio, Mauro Larosa:
  A Graphic Notation for Formal Specifications of Dynamic Systems. 40-61
  
• Graeme Smith:
  A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. 62-81
  
• Anna Mikhajlova, Emil Sekerinski:
  Class Refinement and Interface Refinement in Object-Oriented Programs. 82-101
  
• Stephan Kleuker:
  Formalizing Requirements for Distributed Systems with Trace Diagrams. 102-121
  
• Franz Huber, Bernhard Schätz, Geralf Einert:
  Consistent Graphical Specification of Distributed Systems. 122-141
  
• Kevin Lano, Arturo Sanchez:
  Design of Reactive Control Systems for Event-Drivem Operations. 142-161
  
• Hans Fleischhack, Josef Tapken:
  An M-Net Semantics for a Real-Time Extension of µSDL. 162-181
  
• Manfred Broy, Radu Grosu, Cornel Klein:
  Reconciling Real-Time with Asynchronous Message Passing. 182-200
  
• Martin Schönhoff, Mojgan Kowsari:
  Specifying the Remote Control of Valves in an Explosion Test Environment. 201-220
  
• Lionel Devauchelle, Peter Gorm Larsen, Henrik Voss:
  PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System. 221-236
  
• William D. Young, William R. Bevier:
  Mathematical Modeling and Analysis of an External Memory Manager. 237-257
  
• Paul Mukherjee:
  Automatic Translation of VDM-SL Specifications into Gofer. 258-277
  
• Sten Agerholm, Jacob Frost:
  Towards an Integrated CASE and Theorem Proving Tool for VDM-SL. 278-297
  
• Kevin Lano, Juan Bicarregui, José Luiz Fiadeiro, Antónia Lopes:
  Specification of Required Non-determinism. 298-317
  
• Haykal Tej, Burkhart Wolff:
  A Corrected Failure Divergence Model for CSP in Isabelle/HOL. 318-337
  
• Bernhard K. Aichernig, Peter Gorm Larsen:
  A Proof Obligation Generator for VDM-SL. 338-357
  
• Marc Mehdi Ayadi, Dominique Bolignano:
  Verification of Cryptographic Protocols: An Experiment. 358-377
  
• Jean-Charles Grégoire:
  TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations. 378-397
  
• Abdelillah Mokkedem, Michael J. Ferguson, Robert de B. Johnston:
  A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol. 398-417
  
• J. M. R. Martin, S. A. Jassim:
  An Efficient Technique for Deadlock Analysis of Large Scale Process Networks. 418-441
  
• Shenwei Yu, Zhaohui Luo:
  Implementing a Model Checker for LEGO. 442-458
  
• Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß:
  Formal Verification of Transformations for Peephole Optimization. 459-472
  
• Richard F. Paige:
  A Meta-Method for Formal Method Integration. 473-494
  
• David Hemer, Peter A. Lindsay:
  Reuse of Verified Design Templates Through Extended Pattern Matching. 495-514
  
• Frank S. de Boer, Ulrich Hannemann, Willem P. de Roever:
  A Compositional Proof System for Shared Variable Concurrency. 515-532
  
• Pierre Michel, Virginie Wiels:
  A Framework for Modular Formal Specification and Verification. 533-552
  
• Carsta Petersohn, Luis Urbina:
  A Timed Semantics for the STATEMATE Implementation of Statecharts. 553-572
  
• David W. J. Stringer-Calvert, Susan Stepney, Ian Wand:
  Using PVS to Prove a Z Refinement: A Case Study. 573-588
  
• Pertti Kellomäki:
  Verification of Reactive Systems Using DisCo and PVS. 589-604
  
• David Cazier, Jean-François Dufourd:
  Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects. 605-623
  
• Leila Silva, Augusto Sampaio, Edna Barros:
  A Normal Form Reduction Strategy for Hardware/Software Partitioning. 624-643
  
• Eerke A. Boiten, Howard Bowman, John Derrick, Maarten Steen:
  Viewpoint Consistency in Z and LOTOS: A Case Study. 644-664
  
• Michel Charpentier:
  A UNITY Mapping Operator for Distributed Programs. 665-684