Proceedings of the First International Symposium of Formal Methods Europe: Industrial-Strength Formal Methods
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

FM
DBLP
Scholar
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.