FME '97 Industrial Applications and Strengthened Foundations of Formal Methods 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997. Proceedings

This book constitutes the refereed proceedings of FME '97, the 4th International Symposium of Formal Methods Europe devoted to Industrial Applications and Strengthened Foundations of Formal Methods , held in Graz, Austria, in September 1997. The 35 revised full papers presented in the volume were selected from a total of 94 submissions. Formal methods and mathematically based techniques are increasingly recognized as a viable technology for the development and engineering of computing systems. The majority of the papers in this volume describe industrial applications, extensions to existing techniques, or case studies; papers on theoretical aspects show clear potential applicability.

Diagrams and programming languages for programmable controllers.- Graphical specification and reasoning: Case study generalised railroad crossing.- A graphic notation for formal specifications of dynamic systems.- A semantic integration of object-Z and CSP for the specification of concurrent systems.- Class refinement and interface refinement in object-oriented programs.- Formalizing requirements for distributed systems with trace diagrams.- Consistent graphical specification of distributed systems.- Design of reactive control systems for event-driven operations.- An M-Net semantics for a real-time extension of µSDL.- Reconciling real-time with asynchronous message passing.- Specifying the remote controlling of valves in an explosion test environment.- PICGAL: Practical use of formal specification to develop a complex critical system.- Mathematical modeling and analysis of an external memory manager.- Automatic translation of VDM-SL specifications into gofer.- Towards an Integrated CASE and theorem proving tool for VDM-SL.- Specification of required non-determinism.- A corrected failure-divergence model for CSP in Isabelle/HOL.- A proof obligation generator for VDM-SL.- Verification of cryptographic protocols: An experiment.- TLA + PROMELA: Conjecture, check, proof.- A TLA solution to the specification and verification of the RLP1 retransmission protocol.- An efficient technique for deadlock analysis of large scale process networks.- Implementing a model checker for LEGO.- Formal verification of transformations for peephole optimization.- A meta-method for formal method integration.- Reuse of verified design templates through extended pattern matching.- A compositional proof system for shared variable concurrency.- A framework for modular formal specification andverification.- A timed semantics for the StateMate implementation of statecharts.- Using PVS to prove a Z refinement: A case study.- Verification of reactive systems using DisCo and PVS.- Term rewrite systems to derive set boolean operations on 2D objects.- A normal form reduction strategy for hardware/software partitioning.- Viewpoint consistency in Z and LOTOS: A case study.- A UNITY mapping operator for distributed programs.