+612 9045 4394
Fme 2001: Formal Methods for Increasing Software Productivity : International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings - Jose N. Oliveira

Fme 2001: Formal Methods for Increasing Software Productivity

International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings

By: Jose N. Oliveira (Editor), Pamela Zave (Editor)

Paperback Published: 28th February 2001
ISBN: 9783540417910
Number Of Pages: 634

Share This Book:


or 4 easy payments of $45.32 with Learn more
Ships in 5 to 9 business days

FME 2001 is the tenth in a series of meetings organized every eighteen months by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. It follows four VDM Europe Symposia, four other Formal Methods Europe S- posia, and the 1999 World Congress on Formal Methods in the Development of Computing Systems. These meetings have been notably successful in bringing - gether a community of users, researchers, and developers of precise mathematical methods for software development. FME 2001 took place in Berlin, Germany and was organized by the C- puter Science Department of the Humboldt-Universit¨at zu Berlin. The theme of the symposium was Formal Methods for Increasing Software Productivity. This theme recognizes that formal methods have the potential to do more for industrial software development than enhance software quality { they can also increase productivity at many di erent points in the software life-cycle. The importance of the theme is borne out by the many contributed papers showing how formal methods can make software development more e cient. There is an emphasis on tools that nd errors automatically, or with relatively little human e ort. There is also an emphasis on the use of formal methods to assist with critical, labor-intensive tasks such as program design and test-case generation.

Lightweight Formal Methodsp. 1
Reformulation: A Way to Combine Dynamic Properties and B Refinementp. 2
Mechanized Analysis of Behavioral Conformance in the Eiffel Base Librariesp. 20
Proofs of Correctness of Cache-Coherence Protocolsp. 43
Model-Checking Over Multi-valued Logicsp. 72
How to Make FDR Spin: LTL Model Checking of CSP by Refinementp. 99
Avoiding State Explosion for Distributed Systems with Timestampsp. 119
Secrecy-Preserving Refinementp. 135
Information Flow Control and Applications - Bridging a Gap -p. 153
A Rigorous Approach to Modeling and Analyzing E-Commerce Architecturesp. 173
A Formal Model for Reasoning about Adaptive QoS-Enabled Middlewarep. 197
A Programming Model for Wide-Area Computingp. 222
A Formal Model of Object-Oriented Design and GoF Design Patternsp. 223
Validation of UML Models Thanks to Z and Lustrep. 242
Components, Contracts, and Connectors for the Unified Modelling Language UMLp. 259
An Integrated Approach to Specification and Validation of Real-Time Systemsp. 278
Real-Time Logic Revisitedp. 300
Improvements in BDD-Based Reachability Analysis of Timed Automatap. 318
Serialising Parallel Processes in a Hardware/Software Partitioning Contextp. 344
Verifying Implementation Relationsp. 364
An Adequate Logic for Full LOTOSp. 384
Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics (Mc)p. 396
Faithful Translations among Models and Specificationsp. 419
Composing Contracts: An Adventure in Financial Engineeringp. 435
From Complex Specifications to a Working Prototype. A Protocol Engineering Case Studyp. 436
Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP Systemp. 449
Using Formal Verification Techniques to Reduce Simulation and Test Effortp. 465
Transacted Memory for Smart Cardsp. 478
Houdini, an Annotation Assistant for ESC/Javap. 500
A Heuristic for Symmetry Reductions with Scalarsetsp. 518
View Updatability Based on the Models of a Formal Specificationp. 534
Grammar Adaptationp. 550
Test-Case Calculation through Abstractionp. 571
A Modular Approach to the Specification and Validation of an Electrical Flight Control Systemp. 590
A Combined Testing and Verification Approach for Software Reliabilityp. 611
Author Indexp. 629
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540417910
ISBN-10: 3540417915
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 634
Published: 28th February 2001
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 3.3
Weight (kg): 0.89