ThisvolumecontainstheproceedingsofFM2003,the12thInternationalFormal Methods Europe Symposium which was held in Pisa, Italy on September 8–14, 2003. Formal Methods Europe (FME, www. fmeurope. org) is an independent - sociation which aims to stimulate the use of and research on formal methods for system development. FME conferences began with a VDM Europe symposium in 1987. Since then, the meetings have grown and have been held about once - ery 18 months. Throughout the years the symposia have been notably successful in bringing together researchers, tool developers, vendors, and users, both from academia and from industry. Unlike previous symposia in the series, FM 2003 was not given a speci?c theme. Rather, its main goal could be synthesized as “widening the scope. ” Indeed, the organizers aimed at enlarging the audience and impact of the symposium along several directions. Dropping the su?x ‘E’ from the title of the conference re?ects the wish to welcome participation and contribution from every country; also,contributionsfromoutsidethetraditionalFormalMethodscommunitywere solicited. The recent innovation of including an Industrial Day as an important part of the symposium shows the strong commitment to involve industrial p- ple more and more within the Formal Methods community. Even the traditional and rather fuzzy borderline between “software engineering formal methods” and methods and formalisms exploited in di?erent ?elds of engineering was so- what challenged.
Author(s): Kouichi Kishida (auth.), Keijiro Araki, Stefania Gnesi, Dino Mandrioli (eds.)
Series: Lecture Notes in Computer Science 2805
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003
Language: English
Commentary: Incorrect bookmarks ("Chapter XX" instead of paper titles), double pages (paper "Combining Real-Time Model-Checking and Fault Tree Analysis" appears twice).
Pages: 946
Tags: Logics and Meanings of Programs; Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Mathematical Logic and Formal Languages; Management of Computing and Information Systems
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
