FME 2001: Formal Methods for Increasing Software Productivity: International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, ... (Lecture Notes in Computer Science (2021))

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. FME 2001: Formal Methods for Increasing Software Productivity Preface Acknowledgements Table of Contents Lightweight Formal Methods Reformulation: A Way to Combine Dynamic Properties and B Refinement Introduction Example Operational Description Dynamic Properties Reformulated Dynamic Property Verification About Refinement Refinement and Dynamic Properties Weak Sufficient Conditions Strong Sufficient Conditions Dynamic Properties Reformulation Versus Variants and Loop Invariants Conclusion and Perspectives References Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries Introduction The Eiffel Base Libraries Specification of Library Classes Representation of Class Specifications in unhbox voidb @x hbox {rmfamily Isabelle/HOL}{} The Type of Classes Class Constructors Behavioral Conformance Extra Methods Behavioral Conformance in unhbox voidb @x hbox {rmfamily Isabelle/HOL}{} Transitivity of Conformance Inheritance in the Eiffel Base Libraries{} Subclass Calculation The Subclass Calculator An Alternative Representation of {em Collection} Conformance Analysis of the Eiffel Base Libraries{} Conclusions References Proofs of Correctness of Cache-Coherence Protocols Introduction: Memory Models and Protocols The CRF Memory Model The {Cachet}{} Protocol The Imperative-&-Directive Design Methodology The Writer-Push Protocol The Manual Proof of Correctness Setting Up for the Machine-Assisted Verification Choice of a Logical System Choice of a Tool The Move to PVS Structure of a TLA Specification in PVS Structure of a TLA-Based Proof Example: Derived Rules The Machine-Assisted Proof of WP Soundness Liveness Discussion Model Checking Model-Checking or Theorem-Proving The Structure of the Proof The Abstraction Function A Comparison of the Proofs Summary References Model-Checking over Multi-valued Logics Introduction Example CTL Model-Checking Specifying the Logic Lattice Theory Quasi-Boolean Lattices Multi-valued CTL Model-Checking Defining the Model Multi-valued CTL Chi Chek: A Multi-valued Model-Checker Table Library The Partition Handler Algorithm for Chi Chek Correctness and Termination of Chi Chek Complexity Correctness Conclusion and Future Work References Appendix Lattice Theory Chi CTL Table Library Correctness and Termination How to Make FDR Spin LTL Model Checking of CSP by Refinement Introduction Preliminaries Model Checking Using a Specification and Refinement Model Checking Using a Tester and Composition Tackling Deadlocking Traces Translation of the Tester into CSP Testing Emptiness in CSP/FDR Summary Preservation of LTL under Refinement Complexity, Future Work, and Conclusion References A Simple Example in FDR 2.28 A More Complicated Example in FDR Avoiding State Explosion for Distributed Systems with Timestamps Introduction High Availability and Distributed Systems Managing Resources in a Distributed System Quality of Service and Fault Tolerance Abstraction on Timestamps Timestamps in State Vector Principle Formal Description Implementation Experimental Results Some Results Conclusion and Future Work References Secrecy-Preserving Refinement Introduction Security and Refinement Specification Language Stream-Processing Functions Associating a Stream-Processing Function to a Process Secrecy Refinement Property Refinement Interface Refinement Conditional Refinement A Variant of TLS The Handshake Protocol The Flaw The Fix Implementing Secure Channels Conclusion and Further Work References Information Flow Control and Applications - Bridging a Gap Introduction Information Flow Control Specification Formalism / System Model Flow Policies Formal Definitions of Information Flow Intransitive Information Flow More Applications of Intransitive Information Flow The Problem Towards a Solution A Solution The Solution Revisited Verification Conditions Related Work Conclusion References A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures Introduction Basic Concepts A Theory of Agent-Based Systems Modes of Agents Anatomy of an Agent Formal Notation for Agents Operational Semantics of an Agent Connectors and Configurations Specification of an E-Commerce Architecture - An Example Visual Models Formal Specifications Implementation Details Conclusion References A Appendix I - Larch Traits B Appendix II - Formal Specifications for E-Commerce C Appendix III - Java Code A Formal Model for Reasoning about Adaptive QoS-Enabled Middleware Introduction The Two Level Meta-architecture The QoS Broker Meta-architecture for QoS-Based Services Resource Management Policies for MM Servers Reasoning about QoS-Based MM Services QoS Based MM Service Specifying a Resource Based MM Service A Resource Based MM Behavior Specifying an Adaptive Resource Scheduling Policy for a QoS Broker Related Work and Future Research Directions References A Programming Model for Wide-Area Computing A Formal Model of Object-Oriented Design and GoF Design Patterns Introduction A Formal Model of Object-Oriented Design An Overview of Extended OMT Notation The Formal Model Matching Designs to Patterns Specifying the Properties of the Patterns An Example: Checking an Instantiation of the State Conclusions References Validation of UML Models Thanks to Z and Lustre Introduction The ``Cash-Point'' Service Elaboration of the UML Specification Requirement Capture The Static Part of the Cash-Point Service The Dynamic Part of the Cash-Point Service Validation of the Static Part Generating Z Specifications Using a Prover to Validate the Static Part Validation of the Dynamic Part of UML Model Conclusion References Components, Contracts, and Connectors for the Unified Modelling Language UML Introduction Abstract Behaviour, Interfaces, and Components Actions, Operations, and Their Abstraction The Specification of Interfaces and Components Component Composition Contracts Connectors Semantics for Components Semantics of Actions and Operations Abstraction of Actions and Operations Reasoning about Composition and Contracts Implementing and Refining Abstract Specifications Composition of Components Related Work Conclusions References An Integrated Approach to Specification and Validation of Real-Time Systems Introduction Timed-CSP-Z Formal Specification of the WDT Formal Specification of the OBC The Semantics of Timed-CSP-Z The Specification Analysis: Strategy and Tools Converting Timed-CSP-Z to TER Nets An Analysis Example Conclusion References Real-Time Logic Revisited Introduction The Basic RTL Model Time in RTL Actions, States, and Variables in RTL Many-Sorted Logic The MSL Language An MSL Proof System MSL Models RTL in MSL RTL Theorems Typical Real-Time Requirements in RTL A Shallow Embedding of RTL in PVS Conclusions and Related Work References Improvements in BDD-Based Reachability Analysis of Timed Automata Introduction Cottbus Timed Automata Example Informal Introduction to CTA Modules Timed Automata Examples: CTA Models of a Mutex Protocol and a MOS Circuit Discretization Efficient Verification Using the Structure of the Model Communication Graph and Variable Ordering Upper Bound for the BDD's Size Finding Good Variable Orderings for CTA Models Experimental Results Summary References Serialising Parallel Processes in a Hardware/Software Partitioning Context Introduction A Language of Communicating Processes Some Algebraic Laws and Useful Definitions The Partitioning Approach The Serialisation Strategy The Serialisation Rules The Serialisation Algorithm Implementation Features of the Serialisation Strategy A Simple Example Conclusions References Verifying Implementation Relations Introduction Preliminaries Extraction Patterns Implementation Relations Representing CSP Processes and Extraction Patterns Unambiguous CTS Graph Representation of Implementation Relations Algorithms Concluding Remarks References An Adequate Logic for Full LOTOS Introduction Related Work Structure of the Paper Symbolic Transition Systems Substitution The Modal Logic FULL Bisimulation and Adequacy of FULL Further Work References Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics Prologue Classical Spelling Checker Dictionary Intuitionistic Spelling Checker Dictionary Enter Remove The Pre-conditions Test A Simple Proof Klinik of Doctors and Their Patients Klinik as Fibered Space Epilogue Related Work Conclusions References Faithful Translations among Models and Specifications Introduction The Semantics of Systems and Modules Faithful Translations Issues in Translation Synchrony and Asynchrony Unenabled Transitions Atomicity of Transitions Variables with Unspecified Next Values Partitioning into Components State Extensions Examples of Faithful Translations Operation Refinements Adding Idle Transitions Adding Explicit Failures Data Abstraction Changes in the Branching Structure Conclusions References Composing Contracts: An Adventure in Financial Engineering From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study Introduction Service Description Towards a Formal Model The Formal Design Process System Architecture LOTOS Specification. A Brief Outline Protocol Testing and Validation Simulation and Rapid Prototyping Concluding Remarks References Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System Introduction Modeling and Validation Flows The TMS320C55xTM DSP System The Software Model Test Cases Automatic Generation of Tests Choosing a Coverage Metrics The Esterel Language Formally Evaluating State-Coverage Generation of Test Sequences Taking Environment Constraints into Account From Test Sequences to Test Cases Manual Generation of Test Cases Generation of Test Cases by Pipeline Inversion Pipeline Inversion Our Pipeline Model Pipeline Inversion in Practice Practical Results Module Description Generation of the Initial Reached States Generation of New Test Cases Remarks Bugs Found Conclusions Comparison with Related Works Perspectives References Using Formal Verification Techniques to Reduce Simulation and Test Effort Introduction Methodology and Case Study Identifying and Expressing Properties Identification Formal Expression of the Properties Verifying Properties Formal Verification in Lustre Practical Problems Current Results Conclusion and Future Work References Transacted Memory for Smart Cards Introduction The Process The Idea Abstract Specification First Refinement Data Structures Second Refinement Realistic Constraints Causes of Error States Data Structures SPIN and C Prototype DNewTag in C DNewTag in Promela DTidy Testing and Assertion Checking Lessons Learned Conclusion and Future Work References Houdini, an Annotation Assistant for ESC/Java Introduction Review of ESC/Java Houdini Architecture Generating the Candidate Annotation Set Dealing with Libraries User Interface Experience Other Annotation Assistants Related Work Conclusions References A Heuristic for Symmetry Reductions with Scalarsets Introduction Preliminaries Reduction Strategies Extending Spin with Symmetry Reductions Experimental Results Conclusions and Future Work References View Updatability Based on the Models of a Formal Specification Introduction Category Theoretic Information System Specification Views Updatability Schema Updatability Related Work Conclusion References Grammar Adaptation Introduction Grammar Fragments Standard Context-Free Grammars Deviation Semantics Formal Reasoning Equivalent Grammars Beyond Equivalence Grammar Transformers The Transformation Framework Primitives Combinators Constraints Symbolic Operands The Operator Suite Overview Refactoring Construction Destruction Discussion Concluding Remarks References Test-Case Calculation through Abstraction Introduction Motivation Related Work on Testing Contribution Testing Based on Contracts Contracts Semantics Refinement Test-Cases Are Abstractions Input-Output Tests Partition Tests Testing Interactive Systems User Interaction Iterative Choice Scenarios Calculating Scenarios for Testing Critics on FSM Approaches Compositions Scenario Synthesis Scenario Based Testing Strategies Example: Process Scheduler Interactive Process Scheduler Interaction Partitioning Compositions Scenarios Conclusions References A Modular Approach to the Specification and Validation of an Electrical Flight Control System Introduction The {it VaMoS} Language Modularity in {it VaMoS Language} VaMoS Specification Language Structural Verification Behavior Verification of Modular Specifications Modular Aspects Abstractions Practical Application Example Test Case Generation from Modular Specifications Modular Aspects Practical Application Example Implementation of a CASE Environment Multi-formalism Management Open Platform Note Files Conclusion References A Combined Testing and Verification Approach for Software Reliability Introduction The Combined Methodology: Testing and Verification The Methodology in Practice The Robot Control System Experimental Environment Verification of the RCS Testing and Verification Results Conclusions References Author Index Lightweight Formal Methods / Daniel Jackson -- Reformulation: A Way To Combine Dynamic Properties And B Refinement / F. Bellegarde, C. Darlot And J. Julliand / [and Others] -- Mechanized Analysis Of Behavioral Conformance In The Eiffel Base Libraries / Steffen Helke And Thomas Santen -- Proofs Of Correctness Of Cache-coherence Protocols / Joseph Stoy And Xiaowei Shen / Arvind -- Model-checking Over Multi-valued Logics / Marsha Chechik, Steve Easterbrook And Victor Petrovykh -- How To Make Fdr Spin: Ltl Model Checking Of Csp By Refinement / Michael Leuschel, Thierry Massari And Andrew Currie -- Avoiding State Explosion For Distributed Systems With Timestamps / Fabrice Derepas, Paul Gastin And David Plainfosse. José Nuno Oliveira, Pamela Zave (eds.). Includes Bibliographical References And Index. This book constitutes the refereed proceedings of the International Symposium of Formal Methods Europe, FME 2001, held in Berlin, Germany, in March 2001. The 32 revised full papers presented together with abstracts of three invited talks were carefully reviewed and selected from a total of 72 submissions. Focusing on increasing software productivity, all current aspects in formal methods are covered. Among the application areas addressed are avionics, smart cards, financial engineering, E-commerce, middleware, security, telecommunications, etc.