Research Catalog

Title

FME '93 : industrial-strength formal methods : First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993 proceedings / J.C.P. Woodcock, P.G. Larsen, eds.

Author

International Symposium of Formal Methods Europe (1st : 1993 : Odense, Denmark)

Publication

Berlin ; New York : Springer-Verlag, ©1993.

Items in the Library & Off-site

Details

Additional Authors

• Woodcock, Jim.
• Larsen, P. G. (Peter Gorm), 1964-

Description

xi, 689 pages : illustrations; 24 cm.

Summary

"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.

Series Statement

Lecture notes in computer science ; 670

Uniform Title

Lecture notes in computer science ; 670.

Alternative Title

Formal Methods Europe '93.

Subject

• Computer software > Development > Congresses
• Computer software > Development
• Programmatuurtechniek
• VDM
• Engenharia De Programacao (Software)

Genre/Form

Conference papers and proceedings.

Bibliography (note)

• Includes bibliographical references.

Contents

• Reasoning about Interference in an Object-Based Design Method / C.B. Jones -- Using Relative Refinement for Fault Tolerance / Antonio Cau and Willem-Paul de Roever -- Specification and Validation of a Security Policy Model / Tony Boswell -- Experiences from Applications of RAISE / B. Dandanell, Jesper Gortz, Jan Storbank Pedersen and Eld Zierau -- Role of VDM(++) in the Development of a Real-Time Tracking and Tracing System / E.H. Durr and E.M. Dusink -- The Integration of LOTOS with an Object-Oriented Development Method / Mikael Hedlund -- An Industrial Experience on LOTOS-Based Prototyping for Switching Systems Design / Gonzalo Leon, Juan C. Yelmo, Carlos Sanchez, F. Javier Carrasco and Juan J. Gil.
• Towards an Implementation-oriented Specification of TP Protocol in LOTOS / Ing Widya and Gert-Jan van der Heijden -- A Metalanguage for the Formal Requirement Specification of Reactive Systems / Egidio Astesiano and Gianna Reggio -- Model Checking in Practice: the T9000 Virtual Channel Processor / Geoff Barrett -- Algorithm Refinement with Read and Write Frames / Juan Bicarregui -- Invariants, Frames and Postconditions: a Comparison of the VDM and B Notations / Juan Bicarregui and Brian Ritchie -- The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective / Jonathan Bowen and Victoria Stavridou -- A Proof Environment for Concurrent Programs / Naima Brown and Dominique Mery -- A VDM study of Fault-Tolerant Stable Storage Towards a Computer Engineering Mathematics / Andrew Butterfield.
• Applications of Modal Logic for the Specification of Real-Time Systems / Liang Chen and Alistair Munro -- Formal Methods Reality Check: Industrial Usage / Dan Craigen, Susan Gerhart and Ted Ralston -- Automating the Generation and Sequencing of Test Cases from Model-Based Specifications / Jeremy Dick and Alain Faivre -- The Parallel Abstract Machine: A Common Execution Model for FDTs / Guillaume Doumene Jean-Francois Monin -- Generalizing Abadi & Lamport's Method to Solve a Problem Posed by A. Pnucli / Kai Engelhardt and Willem-Paul de Roever -- Real-Time Refinement / Colin Fidge -- Different FDTs Confronted with Different ODP-Viewpoints of the Trader / Joachim Fischer, Andreas Prinz and Andreas Vogel -- On the Derivation of Executable Database Programs from Formal Specifications / T. Gunther, Klaus-Dieter Schewe and Ingrid Wetzel.
• A Concurrency Case Study using RAISE / Anne Haxthausen and Chris George -- Specifying a Safety-Critical Control System in Z / Jonathan Jacky -- An Overview of the SPRINT Method / H.B.M. Jonkers -- Application of Composition Development Method for Definition of SYNTHESIS Information Resource Query Language Semantics / Leonid Kalinichenko, Nikolaj Nikitchenko and Vladimir Zadorozhny -- Verification Tools in the Development of Provably Correct Compilers / M.R.K. Krishna Rao, P.K. Pandya and R.K. Shyamasundar -- Encoding W: A Logic for Z in 2OBJ / Andrew Martin -- Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned / Sam Owre, John Rushby, Natarajan Shankar and Friedrich von Henke -- Conformity Clause for VDM-SL / Graeme I. Parkin and Brian Wichmann.
• Process Instances in LOTOS Simulation / Simon Pickin, Yan Yang, Wiet Bouma, Sylvie Simon and Tanja de Groot -- The SAZ Project: Integrating SSADM and Z / Fiona Polack, Mark Whiston and Keith Mander -- Maintaining Consistency Under Changes to Formal Specifications / Kelvin J. Ross and Peter A. Lindsay -- An EVES Data Abstraction Example / Mark Saaltink, Sentot Kromodimoeljo, Bill Pase, Dan Craigen and Irwin Meisels -- Putting Advanced Reachability Analysis Techniques Together: the "ARA" Tool / Antti Valmari, Jukka Kemppainen, Matthew Clegg and Mikko Levanto -- Integrating SA/RT with LOTOS / Anthony W. van der Vloedt and Kees Bogaards -- Symbolic Model Checking for Distributed Real-Time Systems / Farn Wang, Aloysius Mok and E. Allen Emerson.
• Adding Specification Constructors to the Refinement Calculus / Nigel Ward -- Selling Formal Methods to Industry / Debora Weber-Wulff -- Tool Descriptions. ProofPower, Mural. IPTES Toolset, The Centaur-VDM environment. IFAD VDM-SL Toolbox, DST-fuzz. The LOTOS Toolbox, Centaur. DisCo, The Boyer-Moore Theorem Prover. B-Toolkit, Pet Dingo. SpecBox, Raise. ExSpect, CADiZ. Design/CPN, PVS. TAV, FDR. ForMooZ.

ISBN

• 3540566627
• 9783540566625
• 0387566627
• 9780387566627

LCCN

93003605

OCLC

• ocm27815065
• 27815065
• SCSB-1982386

Owning Institutions

Princeton University Library