Marie-Claude Gaudel, Jim Woodcock
Proceedings of the Third International Symposium of Formal Methods Europe: Industrial Benefit and Advances in Formal Methods
FME, 1996.

@proceedings{FME-1996,
	address       = "Oxford, England, United Kingdom",
	editor        = "Marie-Claude Gaudel and Jim Woodcock",
	isbn          = "3-540-60973-3",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Third International Symposium of Formal Methods Europe: Industrial Benefit and Advances in Formal Methods}",
	volume        = 1051,
	year          = 1996,
}

Contents (38 items)

11 ×#specification
6 ×#formal method
6 ×#verification
4 ×#case study
4 ×#development
4 ×#safety
3 ×#approach
3 ×#using
2 ×#analysis
2 ×#automation

FME-1996-Hoare #how #proving #question #reliability

How Did Software Get So Reliable Without Proof? (CARH), pp. 1–17.

FME-1996-Sivertsen #case study #development #safety

A Case Study on the Formal Development of a Reactor Safety System (TS), pp. 18–38.

FME-1996-Peleska #automation #industrial #safety #testing

Test Automation for Safety-Critical Systems: Industrial Application and Future Developments (JP), pp. 39–59.

FME-1996-BicarreguiDW #analysis #formal method

Quantitative Analysis of an Application of Formal Methods (JB, JD, EW), pp. 60–73.

FME-1996-HoareDNS #cics

Applying the B Technologies on CICS (JH, JD, DN, IHS), pp. 74–84.

FME-1996-WaldenS

Refining Action Systems within B-Tool (MAW, KS), pp. 85–104.

FME-1996-KasurinenS #specification

Integrating Action Systems and Z in a Medical System Specification (VK, KS), pp. 105–119.

FME-1996-GroenboomSRL #case study #formal method #specification

Formalizing Anaesthesia: a case study in formal specification (RG, ES, ER, GRRdL), pp. 120–139.

FME-1996-MartinsH #evaluation #performance #specification

A New System Engineering Methodology Coupling Formal Specification and Performance Evaluation (JJM, JPH), pp. 140–159.

FME-1996-Vito #formal method #navigation #requirements

Formalizing New Navigation Requirements for NASA’s Space Shuttle (BLDV), pp. 160–178.

FME-1996-FrohlichL #c++ #specification

Combining VDM-SL Specifications with C++ Code (BF, PGL), pp. 179–194.

FME-1996-Clement #abstraction

Data Reification without Explicit Abstraction Functions (TC), pp. 195–213.

FME-1996-BrookesFL #case study #comparative #component #specification

Formal and Informal Specifications of a Secure System Component: Final Results in a Comparative Study (TMB, JSF, PGL), pp. 214–227.

FME-1996-ValmariS #liveness #safety #verification #visual notation

Visual Verification of Safety and Liveness (AV, MS), pp. 228–247.

FME-1996-SchatzHB #consistency #development #specification #visual notation

Graphical Development of Consistent System Specifications (BS, HH, MB), pp. 248–267.

FME-1996-HutterLSSSW #deduction #verification

Deduction in the Verification Support Environment (VSE) (DH, BL, CS, JHS, WS, AW), pp. 268–286.

FME-1996-BoitenDBS #consistency #refinement #specification

Consistency and Refinement for Partial Specification in Z (EAB, JD, HB, MS), pp. 287–306.

FME-1996-Weber #design #safety

Combining Statecharts and Z for the Design of Safety-Critical Control Systems (MW), pp. 307–326.

FME-1996-FidgeUKH #realtime #refinement #scheduling

Integrating Real-Time Scheduling Theory and Program Refinement (CJF, MU, PK, IJH), pp. 327–346.

FME-1996-SeguinW #approach #category theory #fault tolerance #logic #using #validation

Using a Logical and Categorical Approach for the Validation of Fault-Tolerant Systems (CS, VW), pp. 347–366.

FME-1996-BoerH #communication #nondeterminism #process

Local Nondeterminism in Asynchronously Communicating Processes (FSdB, MvH), pp. 367–384.

FME-1996-ChalinGR #identification #interface #specification

Identification of and Solutions to Shortcomings of LCL, a Larch/C Interface Specification Language (PC, PG, TR), pp. 385–404.

FME-1996-KannikeswaranRFAW #algorithm #specification #verification

Formal Specification and Verification of the pGVT Algorithm (BK, RR, PF, PA, PAW), pp. 405–424.

FME-1996-PuglieseT #automation #verification

Automatic Verification of a Hydroelectric Power Plant (RP, ET), pp. 425–444.

FME-1996-Jackson #case study #embedded #experience #scheduling

Experiences in Embedded Scheduling (DMJ), pp. 445–464.

FME-1996-BoigelotG #analysis #model checking #protocol #using

Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN (BB, PG), pp. 465–478.

FME-1996-KleukerT #development #distributed #incremental #specification

The Incremental Development of Correct Specifications for Distributed Systems (SK, HT), pp. 479–498.

FME-1996-George #formal method

A Theory of Distributing Train Rescheduling (CG), pp. 499–517.

FME-1996-ShiN #petri net #specification

An Improved Translation of SA/RT Specification Model to High-Level Timed Petri Nets (LS, PN), pp. 518–537.

FME-1996-PeleskaS #implementation #testing

From Testing Theory to Test Driver Implementation (JP, MS), pp. 538–556.

FME-1996-ComuzziH #slicing #using

Program Slicing Using Weakest Preconditions (JJC, JMH), pp. 557–575.

FME-1996-AlencarL #approach #design pattern #formal method

A Formal Approach to Architectural Design Patterns (PSCA, DDC, CJPdL), pp. 576–594.

FME-1996-ZwiersHLRS #composition #development #reuse #top-down #using

Modular Completeness: Integrating the Reuse of Specified Software in Top-down Program Development (JZ, UH, YL, WPdR, FAS), pp. 595–608.

FME-1996-BohnJ #approach #design

A Strategic Approach to Transformational Design (JB, WJ), pp. 609–628.

FME-1996-KolyangSW #implementation

Correct and User-Friendly Implementations of Transformation Systems (K, TS, BW), pp. 629–648.

FME-1996-ArnoldBR #debugging #embedded #formal method #using

An Example of Use of Formal Methods to Debug an Embedded Software (AA, DB, JPR), pp. 649–661.

FME-1996-HavelundS #model checking #protocol #proving #theorem proving #verification

Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.

FME-1996-WangL #concurrent #realtime #verification

Procedure-Level Verification of Real-time Concurrent Systems (FW, CTDL), pp. 682–701.