Diagrams and Programming Languages for Programmable Controllers / Stuart Anderson, Konstantinos Tourlas
Graphical Specification and Reasoning: Case Study Generalised Railroad
Crossing / Henning Dierks, Cheryl Dietz
A Graphic Notation for Formal Specifications of Dynamic Systems / Gianna Reggio, Mauro Larosa
A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems / Graeme Smith
Class Refinement and Interface Refinement in Object-Oriented Programs / Anna Mikhajlova, Emil Sekerinski
Formalizing Requirements for Distributed Systems with Trace Diagrams / Stephan Kleuker
Consistent Graphical Specification of Distributed Systems / Franz Huber, Bernhard Schätz, Geralf Einert
Design of Reactive Control Systems for Event-Driven Operations / K. Lano, A. Sanchez
An M-Net Semantics for a Real-Time Extension of µSDL / Hans Fleischhack, Josef Tapken
Reconciling Real-Time with Asynchronous Message Passing / M. Broy, R. Grosu, C. Klein
Specifying the Remote Controlling of Valves in an Explosion Test Environment / Martin Schönhoff, Mojgan Kowsari
PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System / Lionel Devauchelle, Peter Gorm Larsen, Henrik Voss
Mathematical Modeling and Analysis of an External Memory Manager / William D. Young, William R. Bevier
Automatic Translation of VDM-SL Specifications into Gofer / Paul Mukherjee
Towards an Integrated CASE and Theorem Proving Tool for VDM-SL / Sten Agerholm, Jacob Frost
Specification of Required Non-determinism / K. Lano, J. Bicarregui, J. Fiadeiro, A. Lopes
A Corrected Failure-Divergence Model for CSP in Isabelle/HOL / H. Tej, B. Wolff
A Proof Obligation Generator for VDM-SL / Bernhard K. Aiehernig, Peter Gorm Larsen
Verification of Cryptographic Protocols: An Experiment / Marc Mehdi Ayadi, Dominique Bolignano
TLA + PROMELA: Conjecture, Check, Proof. Engineering New Protocols Using Methods and Formal Notations / J.-Ch. Grdgoire
A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol / Abdelillah Mokkedem, Michael J. Ferguson, Robert deB. Johnston
An Efficient Technique for Deadlock Analysis of Large Scale Process Networks / J.M.R. Martin, S.A. Jassim
Implementing a Model Checker for LEGO / Shenwei Yu, Zhaohui Luo
Formal Verification of Transformations for Peephole Optimization / A. Dold, F.W. von Henke, H. Pfeifer, H. Rueß
A Meta-Method for Formal Method Integration / Richard F. Paige
Reuse of Verified Design Templates Through Extended Pattern Matching / David Hemer, Peter A. Lindsay
A Compositional Proof System for Shared Variable Concurrency / F.S. de Boer, U. Hannemann, W.-P. de Roever
A Framework for Modular Formal Specification and Verification / Pierre Michel, Virginie Wiels
A Timed Semantics for the STATEMATE Implementation of Statecharts / Carsta Petersohn, Luis Urbina
Using PVS to Prove a Z Refinement: A Case Study / David W.J. Stringer-Calvert, Susan Stepney, Ian Wand
Verification of Reactive Systems Using DisCo and PVS / Pertti Kellomdki
Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects / David Cazier, Jean-Franfois Dufourd
A Normal Form Reduction Strategy for Hardware/Software Partitioning / Leila Silva, Augusto Sampaio, Edna Barros
Viewpoint Consistency in Z and LOTOS: A Case Study / Eerke Boiten, Howard Bowman, John Derrick, Maarten Steen
A UNITY Mapping Operator for Distributed Programs / Michel Charpentier
Author Index
