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.
Author(s): Daniel Jackson (auth.), José Nuno Oliveira, Pamela Zave (eds.)
Series: Lecture Notes in Computer Science 2021
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2001
Language: English
Commentary: Incorrect bookmarks (missing top-level texts)
Pages: 634
Tags: Logics and Meanings of Programs; Software Engineering; Mathematical Logic and Formal Languages; Business Information Systems
Lightweight Formal Methods....Pages 1-1
Reformulation: a Way to Combine Dynamic Properties and B Refinement....Pages 2-19
Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries....Pages 20-42
Proofs of Correctness of Cache-Coherence Protocols....Pages 43-71
Model-Checking Over Multi-Valued Logics....Pages 72-98
How to Make FDR Spin LTL Model Checking of CSP by Refinement....Pages 99-118
Avoiding State Explosion for Distributed Systems with Timestamps....Pages 119-134
Secrecy-Preserving Refinement....Pages 135-152
Information Flow Control and Applications — Bridging a Gap —....Pages 153-172
A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures....Pages 173-196
A Formal Model for Reasoning About Adaptive QoS-Enabled Middleware....Pages 197-221
A Programming Model for Wide-Area Computing....Pages 222-222
A Formal Model of Object-Oriented Design and GoF Design Patterns....Pages 223-241
Validation of UML Models Thanks to Z and Lustre....Pages 242-258
Components, Contracts, and Connectors for the Unified Modelling Language UML....Pages 259-277
An Integrated Approach to Specification and Validation of Real-Time Systems....Pages 278-299
Real-Time Logic Revisited....Pages 300-317
Improvements in BDD-Based Reachability Analysis of Timed Automata....Pages 318-343
Serialising Parallel Processes in a Hardware/Software Partitioning Context....Pages 344-363
Verifying Implementation Relations....Pages 364-383
An Adequate Logic for Full LOTOS....Pages 384-395
Faithful Translations Among Models and Specifications....Pages 396-418
Composing Contracts: An Adventure in Financial Engineering....Pages 419-434
From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study....Pages 435-435
Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System....Pages 436-448
Using Formal Verification Techniques to Reduce Simulation and Test Effort....Pages 449-464
Transacted Memory for Smart Cards....Pages 465-477
Houdini, an Annotation Assistant for ESC/Java....Pages 478-499
A Heuristic for Symmetry Reductions with Scalarsets....Pages 500-517
View Updatability Based on the Models of a Formal Specification....Pages 518-533
Grammar Adaptation....Pages 534-549
Test-Case Calculation Through Abstraction....Pages 550-570
A Modular Approach to the Specification and Validation of an Electrical Flight Control System....Pages 571-589
A Combined Testing and Verification Approach for Software Reliability....Pages 590-610
....Pages 611-628
