John S. Fitzgerald, Cliff B. Jones, Peter Lucas
Proceedings of the Fourth International Symposium of Formal Methods Europe: Industrial Applications and Strengthened Foundations of Formal Methods
FME, 1997.

@proceedings{FME-1997,
	address       = "Graz, Austria",
	editor        = "John S. Fitzgerald and Cliff B. Jones and Peter Lucas",
	isbn          = "3-540-63533-5",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Symposium of Formal Methods Europe: Industrial Applications and Strengthened Foundations of Formal Methods}",
	volume        = 1313,
	year          = 1997,
}

Contents (35 items)

10 ×#specification
5 ×#verification
4 ×#proving
3 ×#case study
3 ×#concurrent
3 ×#distributed
3 ×#protocol
3 ×#semantics
3 ×#using
2 ×#analysis

FME-1997-AndersonT #diagrams #programmable #programming language

Diagrams and Programming Languages for Programmable Controllers (SA, KT), pp. 1–19.

FME-1997-DierksD #case study #reasoning #specification #visual notation

Graphical Specification and Reasoning: Case Study Generalised Railroad Crossing (HD, CD), pp. 20–39.

FME-1997-ReggioL #specification

A Graphic Notation for Formal Specifications of Dynamic Systems (GR, ML), pp. 40–61.

FME-1997-Smith #concurrent #csp #integration #semantics #specification

A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems (GS), pp. 62–81.

FME-1997-MikhajlovaS #interface #object-oriented #refinement #source code

Class Refinement and Interface Refinement in Object-Oriented Programs (AM, ES), pp. 82–101.

FME-1997-Kleuker #diagrams #distributed #formal method #requirements

Formalizing Requirements for Distributed Systems with Trace Diagrams (SK), pp. 102–121.

FME-1997-HuberSE #consistency #distributed #specification #visual notation

Consistent Graphical Specification of Distributed Systems (FH, BS, GE), pp. 122–141.

FME-1997-LanoS #design

Design of Reactive Control Systems for Event-Drivem Operations (KL, AS), pp. 142–161.

FME-1997-FleischhackT #realtime #semantics

An M-Net Semantics for a Real-Time Extension of μSDL (HF, JT), pp. 162–181.

FME-1997-BroyGK #message passing #realtime

Reconciling Real-Time with Asynchronous Message Passing (MB, RG, CK), pp. 182–200.

FME-1997-SchonhoffK #explosion #specification #testing

Specifying the Remote Control of Valves in an Explosion Test Environment (MS, MK), pp. 201–220.

FME-1997-DevauchelleLV #named #specification #using

PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System (LD, PGL, HV), pp. 221–236.

FME-1997-YoungB #analysis #memory management #modelling

Mathematical Modeling and Analysis of an External Memory Manager (WDY, WRB), pp. 237–257.

FME-1997-Mukherjee #automation #specification

Automatic Translation of VDM-SL Specifications into Gofer (PM), pp. 258–277.

FME-1997-AgerholmF #automation #proving #theorem proving #towards

Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.

FME-1997-LanoBFL #nondeterminism #specification

Specification of Required Non-determinism (KL, JB, JLF, AL), pp. 298–317.

FME-1997-TejW #csp #higher-order

A Corrected Failure Divergence Model for CSP in Isabelle/HOL (HT, BW), pp. 318–337.

FME-1997-AichernigL #generative #proving

A Proof Obligation Generator for VDM-SL (BKA, PGL), pp. 338–357.

FME-1997-AyadiB #empirical #encryption #protocol #verification

Verification of Cryptographic Protocols: An Experiment (MMA, DB), pp. 358–377.

FME-1997-Gregoire #protocol #proving #using

TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations (JCG), pp. 378–397.

FME-1997-MokkedemFJ #protocol #specification #verification

A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol (AM, MJF, RdBJ), pp. 398–417.

FME-1997-MartinJ #analysis #concurrent #network #performance #process #scalability

An Efficient Technique for Deadlock Analysis of Large Scale Process Networks (JMRM, SAJ), pp. 418–441.

FME-1997-YuL #implementation #model checking

Implementing a Model Checker for LEGO (SY, ZL), pp. 442–458.

FME-1997-DoldHPR #optimisation #verification

Formal Verification of Transformations for Peephole Optimization (AD, FWvH, HP, HR), pp. 459–472.

FME-1997-Paige #formal method #integration

A Meta-Method for Formal Method Integration (RFP), pp. 473–494.

FME-1997-HemerL #design #pattern matching #reuse #using

Reuse of Verified Design Templates Through Extended Pattern Matching (DH, PAL), pp. 495–514.

FME-1997-BoerHR #composition #concurrent #proving

A Compositional Proof System for Shared Variable Concurrency (FSdB, UH, WPdR), pp. 515–532.

FME-1997-MichelW #composition #framework #specification #verification

A Framework for Modular Formal Specification and Verification (PM, VW), pp. 533–552.

FME-1997-PetersohnU #implementation #semantics

A Timed Semantics for the STATEMATE Implementation of Statecharts (CP, LU), pp. 553–572.

FME-1997-Stringer-CalvertSW #case study #refinement #using

Using PVS to Prove a Z Refinement: A Case Study (DWJSC, SS, IW), pp. 573–588.

FME-1997-Kellomaki #using #verification

Verification of Reactive Systems Using DisCo and PVS (PK), pp. 589–604.

FME-1997-CazierD #2d #set #term rewriting

Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects (DC, JFD), pp. 605–623.

FME-1997-SilvaSB #clustering #hardware #normalisation #reduction

A Normal Form Reduction Strategy for Hardware/Software Partitioning (LS, AS, EB), pp. 624–643.

FME-1997-BoitenBDS #case study #consistency

Viewpoint Consistency in Z and LOTOS: A Case Study (EAB, HB, JD, MS), pp. 644–664.

FME-1997-Charpentier #distributed #source code

A UNITY Mapping Operator for Distributed Programs (MC), pp. 665–684.