FME 2003 : formal methods : International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003 : proceedings / Keijiro Araki, Stefania Gnesi, Dino Mandrioli.

With bibliographical references and index.

This book constitutes the refereed proceedings of the International Symposium of Formal Methods Europe, FME 2003, held in Pisa, Italy in September 2003. The 44 revised full papers presented together with 5 invited papers were carefully reviewed and selected from 144 submissions. The papers are organized in topical sections on industrial issues, control systems and applications, communication system verfication, co-specification and compilers, composition, Java, object-orientation and modularity, model checking, parallel processes, program checking and testing, B method, and security.

Invited Speakers -- Looking Back to the Future -- Past, Present, and Future of SRA Implementation of CafeOBJ -- On Failures and Faults -- Trends in Software Verification -- Event Based Sequential Program Development: Application to Constructing a Pointer Program -- I-Day -- Proving the Shalls -- Adaptable Translator of B Specifications to Embedded C Programs -- Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle -- Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project -- Control Systems and Industrial Applications -- Determining the Specification of a Control System from That of Its Environment -- Managerial Issues for the Consideration and Use of Formal Methods -- Verifying Emulation of Legacy Mission Computer Systems -- Improving Safety Assessment of Complex Systems: An Industrial Case Study -- Communications System Verification -- Compositional Verification of an ATM Protocol -- Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method -- Synthesis and Verification of Constraints in the PGM Protocol -- Co-specification and Compilers -- Mapping Statecharts to Verilog for Hardware/Software Co-specification -- A Strategy for Compiling Classes, Inheritance, and Dynamic Binding -- Composition -- A Semantic Foundation for TCOZ in Unifying Theories of Programming -- Refinement and Verification of Synchronized Component-Based Systems -- Certifying and Synthesizing Membership Equational Proofs -- Team Automata Satisfying Compositionality -- Composing Invariants -- Java, Object Orientation and Modularity -- Java Applet Correctness: A Developer-Oriented Approach -- Improving JML: For a Safer and More Effective Language -- Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems -- A Formal Framework for Modular Synchronous System Design -- Model Checking -- Generating Counterexamples for Multi-valued Model-Checking -- Combining Real-Time Model-Checking and Fault Tree Analysis -- Model-Checking TRIO Specifications in SPIN -- Computing Meta-transitions for Linear Transition Systems with Polynomials -- Translation-Based Compositional Reasoning for Software Systems -- Watchdog Transformations for Property-Oriented Model-Checking -- Parallel Process -- A Circus Semantics for Ravenscar Protected Objects -- Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach -- A General Approach to Deadlock Freedom Verification for Software Architectures -- Taking Alloy to the Movies -- Interacting State Machines for Mobility -- Composing Temporal-Logic Specifications with Machine Assistance -- Program Checking and Testing -- Model Checking FTA -- Program Checking with Certificates: Separating Correctness-Critical Code -- Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study -- Checking and Reasoning about Semantic Web through Alloy -- B Method -- Structuring Retrenchments in B by Decomposition -- Design of an Automatic Prover Dedicated to the Refinement of Database Applications -- ProB: A Model Checker for B -- Security -- SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis -- Correctness of Source-Level Safety Policies -- A Topological Characterization of TCP/IP Security.