Jim Woodcock, Peter Gorm Larsen
Proceedings of the First International Symposium of Formal Methods Europe: Industrial-Strength Formal Methods
FME, 1993.

@proceedings{FME-1993,
	address       = "Odense, Denmark",
	editor        = "Jim Woodcock and Peter Gorm Larsen",
	isbn          = "3-540-56662-7",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the First International Symposium of Formal Methods Europe: Industrial-Strength Formal Methods}",
	volume        = 670,
	year          = 1993,
}

Contents (40 items)

9 ×#specification
4 ×#development
4 ×#industrial
4 ×#realtime
4 ×#refinement
3 ×#fault tolerance
3 ×#formal method
2 ×#concurrent
2 ×#design
2 ×#execution

FME-1993-Jones #design #reasoning

Reasoning about Interference in an Object-Based Design Method (CBJ), pp. 1–18.

FME-1993-CauR #fault tolerance #refinement #using

Using Relative Refinement for Fault Tolerance (AC, WPdR), pp. 19–41.

FME-1993-Boswell #policy #security #specification #validation

Specification and Validation of a Security Policy Model (AB), pp. 42–51.

FME-1993-DandanellGPZ #experience

Experience from Applications of RAISE (BD, JG, JSP, EZ), pp. 52–63.

FME-1993-DurrD #development #realtime

Role of VDM(++) in the Development of a Real-Time Tracking and Tracing System (ED, EMD), pp. 64–72.

FME-1993-Hedlund #development #integration #object-oriented

The Integration of LOTOS with an Object Oriented Development Method (MH), pp. 73–82.

FME-1993-LeonYSCG #design #experience #industrial #prototype

An Industrial Experience on LOTOS-Based Prototyping for Switching Systems Design (GL, JCY, CS, FJC, JJG), pp. 83–92.

FME-1993-WidyaH #protocol #specification #towards

Towards an Implementation-oriented Specification of TP Protocol in LOTOS (IW, GJvdH), pp. 93–109.

FME-1993-AstesianoR #metalanguage #specification

A Metalanguage for the Formal Requirement Specification of Reactive Systems (EA, GR), pp. 110–128.

FME-1993-Barrett #model checking

Model Checking in Practice — The T9000 Virtual Channel Processor (GB), pp. 129–147.

FME-1993-Bicarregui #algorithm #refinement

Algorithm Refinement with Read and Write Frames (JB), pp. 148–161.

FME-1993-BicarreguiR #comparison #invariant

Invariants, Frames and Postconditions: a Comparison of the VDM and B Notations (JB, BR), pp. 162–182.

FME-1993-BowenS #formal method #industrial #perspective #safety

The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective (JPB, VS), pp. 183–195.

FME-1993-BrownM #concurrent #proving #source code

A Proof Environment for Concurrent Programs (NB, DM), pp. 196–215.

FME-1993-Butterfield #fault tolerance #towards

A VDM Study of Fault-Tolerant Stable Storage — Towards a Computer Engineering Mathematics (AB), pp. 216–234.

FME-1993-ChenM #logic #realtime #specification

Applications of Modal Logic for the Specification of Real-Time Systems (LC, AM), pp. 235–249.

FME-1993-CraigenGR #formal method #industrial

Formal Methods Reality Check: Industrial Usage (DC, SLG, TR), pp. 250–267.

FME-1993-DickF #automation #generative #modelling #specification #testing

Automating the Generation and Sequencing of Test Cases from Model-Based Specifications (JD, AF), pp. 268–284.

FME-1993-DoumencM #automaton #execution #parallel

The Parallel Abstract Machine: A Common Execution Model for FDTs (GD, JFM), pp. 285–293.

FME-1993-EngelhardtR #problem

Generalizing Abadi & Lamport’s Method to Solve a Problem Posed by A. Pnueli (KE, WPdR), pp. 294–313.

FME-1993-Fidge #realtime #refinement

Real-Time Refinement (CJF), pp. 314–331.

FME-1993-FischerPV

Different FDT’s Confronted with Different ODP-Viewpoints of the Trader (JF, AP, AV), pp. 332–350.

FME-1993-GuntherSW #database #execution #on the #source code #specification

On the Derivation of Executable Database Programs from Formal Specifications (TG, KDS, IW), pp. 351–366.

FME-1993-HaxthausenG #case study #concurrent #using

A Concurrency Case Study Using RAISE (AEH, CG), pp. 367–387.

FME-1993-Jacky #safety #specification

Specifying a Safety-Critical Control System in Z (JJ), pp. 388–402.

FME-1993-Jonkers #overview

An Overview of the SPRINT Method (HBMJ), pp. 403–427.

FME-1993-KalinichenkoNZ #composition #development #query #semantics #synthesis

Application of Composition Development Method for definition of SYNTHESIS information resource query language semantics (LAK, NSN, VZ), pp. 428–441.

FME-1993-RaoPS #compilation #development #tool support #verification

Verification Tools in the Development of Provably Correct Compilers (MRKKR, PKP, RKS), pp. 442–461.

FME-1993-Martin #encoding #logic

Encoding W: A Logic for Z in 2OBJ (AM), pp. 462–481.

FME-1993-OwreRSH #architecture #fault tolerance #lessons learnt #verification

Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned (SO, JMR, NS, FWvH), pp. 482–500.

FME-1993-ParkinW

Conformity Clause for VDM-SL (GIP, BAW), pp. 501–520.

FME-1993-PickinYBSG #process #simulation

Process Instances in LOTOS Simulation (SP, YY, WB, SS, TdG), pp. 521–540.

FME-1993-PolackWM

The SAZ Project: Integrating SSADM and Z. (FP, MW, KM), pp. 541–557.

FME-1993-RossL #consistency #maintenance #specification

Maintaining Consistency Under Changes to Formal Specifications (KJR, PAL), pp. 558–577.

FME-1993-SaaltinkKPCM #abstraction

An EVES Data Abstraction Example (MS, SK, BP, DC, IM), pp. 578–596.

FME-1993-ValmariKCL #analysis #reachability

Putting Advanced Reachability Analysis Techniques Together: the “ARA” Tool (AV, JK, MC, ML), pp. 597–616.

FME-1993-VloedtB

Integrating SA/RT with LOTOS (TvdV, KB), pp. 617–631.

FME-1993-WangME #distributed #model checking #realtime

Symbolic Model Checking for Distributed Real-Time Systems (FW, AKM, EAE), pp. 632–651.

FME-1993-Ward #calculus #refinement #specification

Adding Specification Constructors to the Refinement Calculus (NW), pp. 652–670.

FME-1993-Weber-Wulff #formal method #industrial

Selling Formal Methods to Industry (DWW), pp. 671–678.