FME 2003: Formal Methods: International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003. Proceedings

Front Matter....Pages I-XV
Looking Back to the Future....Pages 1-6
Past, Present, and Future of SRA Implementation of CafeOBJ ....Pages 7-17
On Failures and Faults....Pages 18-39
Trends in Software Verification....Pages 40-50
Event Based Sequential Program Development: Application to Constructing a Pointer Program....Pages 51-74
Proving the Shalls....Pages 75-93
Adaptable Translator of B Specifications to Embedded C Programs....Pages 94-113
Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle....Pages 114-132
Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project....Pages 133-153
Determining the Specification of a Control System from That of Its Environment....Pages 154-169
Managerial Issues for the Consideration and Use of Formal Methods....Pages 170-186
Verifying Emulation of Legacy Mission Computer Systems....Pages 187-207
Improving Safety Assessment of Complex Systems: An Industrial Case Study....Pages 208-222
Compositional Verification of an ATM Protocol....Pages 223-243
Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method....Pages 244-263
Synthesis and Verification of Constraints in the PGM Protocol....Pages 264-281
Mapping Statecharts to Verilog for Hardware/Software Co-specification....Pages 282-300
A Strategy for Compiling Classes, Inheritance, and Dynamic Binding....Pages 301-320
A Semantic Foundation for TCOZ in Unifying Theories of Programming....Pages 321-340
Refinement and Verification of Synchronized Component-Based Systems....Pages 341-358
Certifying and Synthesizing Membership Equational Proofs....Pages 359-380
Team Automata Satisfying Compositionality....Pages 381-400
Composing Invariants....Pages 401-421
Java Applet Correctness: A Developer-Oriented Approach....Pages 422-439
Improving JML: For a Safer and More Effective Language....Pages 440-461
Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems....Pages 462-481
A Formal Framework for Modular Synchronous System Design....Pages 482-502
Generating Counterexamples for Multi-valued Model-Checking....Pages 503-521
Combining Real-Time Model-Checking and Fault Tree Analysis....Pages 522-541
Model-Checking TRIO Specifications in SPIN....Pages 542-561
Computing Meta-transitions for Linear Transition Systems with Polynomials....Pages 562-581
Translation-Based Compositional Reasoning for Software Systems....Pages 582-599
Watchdog Transformations for Property-Oriented Model-Checking....Pages 600-616
A Circus Semantics for Ravenscar Protected Objects....Pages 617-635
Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach....Pages 636-657
A General Approach to Deadlock Freedom Verification for Software Architectures....Pages 658-677
Taking Alloy to the Movies....Pages 678-697
Interacting State Machines for Mobility....Pages 698-718
Composing Temporal-Logic Specifications with Machine Assistance....Pages 719-738
Model Checking FTA....Pages 739-757
Program Checking with Certificates: Separating Correctness-Critical Code....Pages 758-777
Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study....Pages 778-795
Checking and Reasoning about Semantic Web through Alloy....Pages 796-813
Structuring Retrenchments in B by Decomposition....Pages 814-833
Design of an Automatic Prover Dedicated to the Refinement of Database Applications....Pages 834-854
ProB: A Model Checker for B....Pages 855-874
SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis....Pages 875-893
Correctness of Source-Level Safety Policies....Pages 894-913
A Topological Characterization of TCP/IP Security....Pages 914-939
Back Matter....Pages 941-942