FME '93: Industrial-Strength Formal Methods: First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993. Proceedings (Lecture Notes in Computer Science (670))

"The last few years have borne witness to a remarkable diversity of formal methods, with applications to sequential and concurrent software, to real-time and reactive systems, and to hardware design. In that time, many theoretical problems have been tackled and solved, and many continue to be worked upon. Yet it is by the suitability of their industrial application and the extent of their usage that formal methods will ultimately be judged. This volume presents the proceedings of the first international symposium of Formal Methods Europe, FME'93. The symposium focuses on the application of industrial-strength formal methods. Authors address the difficulties of scaling their techniques up to industrial-sized problems, and their suitability in the workplace, and discuss techniques that are formal (that is, they have a mathematical basis) and that are industrially applicable. The volume has four parts: - Invited lectures, containing a lecture by Cliff B. Jones and a lecture by Antonio Cau and Willem-Paul de Roever; - Industrial usage reports, containing 6 reports; - Papers, containing 32 selected and refereedpapers; - Tool descriptions, containing 11 descriptions."--PUBLISHER'S WEBSITE Reasoning about interference in an object-based design method....Pages 1-18 Using relative refinement for fault tolerance....Pages 19-41 Specification and validation of a security policy model....Pages 42-51 Experiences from applications of RAISE....Pages 52-63 Role of VDM(++) in the development of a real-time tracking and tracing system....Pages 64-72 The integration of LOTOS with an object oriented development method....Pages 73-82 An industrial experience on LOTOS-based prototyping for switching systems design....Pages 83-92 Towards an implementation-oriented specification of TP protocol in LOTOS....Pages 93-109 A metalanguage for the formal requirement specification of reactive systems....Pages 110-128 Model checking in practice....Pages 129-147 Algorithm refinement with read and write frames....Pages 148-161 Invariants, frames and postconditions: a comparison of the VDM and B notations....Pages 162-182 The industrial take-up of formal methods in safety-critical and other areas: A perspective....Pages 183-195 A proof environment for concurrent programs....Pages 196-215 A VDM ♣ study of Fault-Tolerant stable storage — Towards a computer engineering mathematics....Pages 216-234 Applications of modal logic for the specification of real-time systems....Pages 235-249 Formal methods reality check: Industrial usage....Pages 250-267 Automating the generation and sequencing of test cases from model-based specifications....Pages 268-284 The parallel abstract machine: A common execution model for FDTs....Pages 285-293 Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli....Pages 294-313 Real-time refinement....Pages 314-331 Different FDT's confronted with different ODP-viewpoints of the trader....Pages 332-350 On the derivation of executable database programs from formal specifications....Pages 351-366 A concurrency case study using RAISE....Pages 367-387 Specifying a safety-critical control system in Z....Pages 388-402 An overview of the SPRINT method....Pages 403-427 Application of composition development method for definition of SYNTHESIS information resource query language semantics....Pages 428-441 Verification tools in the development of provably correct compilers....Pages 442-461 Encoding $$\mathcal{W}$$ : A Logic for Z in 2OBJ....Pages 462-481 Formal verification for fault-tolerant architectures: Some lessons learned....Pages 482-500 Conformity clause for VDM-SL....Pages 501-520 Process instances in LOTOS simulation....Pages 521-540 The SAZ project: Integrating SSADM and Z....Pages 541-557 Maintaining consistency under changes to formal specifications....Pages 558-577 An EVES data abstraction example....Pages 578-596 Putting advanced reachability analysis techniques together: The “ARA” tool....Pages 597-616 Integrating SA/RT with LOTOS....Pages 617-631 Symbolic model checking for distributed real-time systems....Pages 632-651 Adding specification constructors to the refinement calculus....Pages 652-670 Selling formal methods to industry....Pages 671-678 Tool Descriptions....Pages 679-689

the Last Few Years Have Borne Witness To A Remarkable Diversity Of Formal Methods, With Applications To Sequential And Concurrent Software, To Real-time And Reactive Systems,
and To Hardware Design. In That Time, Many Theoretical Problems Have Been Tackled And Solved, And Many Continue To Be Worked Upon. Yet It Is By The Suitability Of Their Industrial Application And The Extent Of Their Usage That Formal Methods Will Ultimately Be Judged.
this Volume Presents The Proceedings Of The First International Symposium Of Formal Methods Europe, Fme'93.
the Symposium Focuses On The Application Of Industrial-strength Formal Methods. Authors Address The Difficulties Of Scaling Their Techniques Up To Industrial-sized Problems, And Their Suitability In The Workplace, And Discuss Techniques That Are Formal (that Is, They Have A Mathematical Basis) And That Are Industrially Applicable.
the Volume Has Four Parts:
- Invited Lectures, Containing A Lecture By Cliff B. Jones And A Lecture By Antonio Cau And Willem-paul De Roever;
- Industrial Usage Reports, Containing 6 Reports;
- Papers, Containing 32 Selected And Refereedpapers;
- Tool Descriptions, Containing 11 Descriptions.

Annotation The last few years have borne witness to a remarkablediversity of formal methods, with applications to sequentialand concurrent software, to real-time and reactive systems, and to hardware design. In that time, many theoreticalproblems have been tackled and solved, and many continue tobe worked upon. Yet it is by the suitability of theirindustrial application and the extent of their usage thatformal methods will ultimately be judged. This volume presents the proceedings of the firstinternational symposium of Formal Methods Europe, FME'93. The symposium focuses on the application ofindustrial-strength formal methods. Authors address thedifficulties of scaling their techniques up toindustrial-sized problems, and their suitability in theworkplace, and discuss techniques that are formal (thatis, they have a mathematical basis) and that areindustrially applicable. The volume has four parts:- Invited lectures, containing a lecture by Cliff B. Jonesand a lecture by Antonio Cau and Willem-Paul de Roever;- Industrial usage reports, containing 6 reports;- Papers, containing 32 selected and refereedpapers;- Tool descriptions, containing 11 descriptions Development of any large computer system is difficult but formal methods like VDM have been shown to help control the development process - and provide useful documentation - of sequential systems.