This volume contains the proceedings of Formal Methods 2005, the 13th InternationalSymposiumonFormalMethodsheldinNewcastleuponTyne,UK, during July 18–22, 2005. Formal Methods Europe (FME, www.fmeurope.org) is an independent association 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 every 18 months. Throughout the years the symposia have been notablysuccessfulinbringingtogetherresearchers,tooldevelopers,vendors,and users, both from academia and from industry. Formal Methods 2005 con?rms this success. We received 130 submissions to the main conference, from all over the world. Each submission was carefully refereed by at least three reviewers. Then, after an intensive, in-depth discussion, the Program Committee selected 31 papers for presentation at the conference. They form the bulk of this volume. We would like to thank all the Program Committee members and the referees for their excellent and e?cient work. Apart from the selected contributions, the Committee invited three keynote lectures from Mathai Joseph, Marie-Claude Gaudel and Chris Johnson. You will ?nd the abstracts/papers for their keynote lectures in this volume as well. AninnovationfortheFM2005programwasapaneldiscussiononthehistory of formal methods, with Jean-Raymond Abrial, Dines Bjørner, Jim Horning and Cli? Jones as panelists. Unfortunately, it was not possible to re?ect this event in the current volume, but you will ?nd the material documenting it elsewhere (see the conference Web page).
Author(s): Mathai Joseph (auth.), John Fitzgerald, Ian J. Hayes, Andrzej Tarlecki (eds.)
Series: Lecture Notes in Computer Science 3582 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 558
Tags: Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Programming Techniques; Mathematical Logic and Formal Languages; Management of Computing and Information Systems
Front Matter....Pages -
Formal Aids for the Growth of Software Systems....Pages 1-1
Formal Methods and Testing: Hypotheses, and Correctness Approximations....Pages 2-8
The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions....Pages 9-25
Modular Verification of Static Class Invariants....Pages 26-42
Decoupling in Object Orientation....Pages 43-58
Controlling Object Allocation Using Creation Guards....Pages 59-74
Symbolic Animation of JML Specifications....Pages 75-90
Certified Memory Usage Analysis....Pages 91-106
Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs....Pages 107-122
Formally Defining and Verifying Master/Slave Speculative Parallelization....Pages 123-138
Systematic Implementation of Real-Time Models....Pages 139-156
Timing Tolerances in Safety-Critical Software....Pages 157-172
Timed Testing with TorX....Pages 173-188
Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems....Pages 189-204
Adding Conflict and Confusion to CSP....Pages 205-220
Combining CSP and B for Specification and Property Verification....Pages 221-236
Operational Semantics for Model Checking Circus ....Pages 237-252
Control Law Diagrams in Circus ....Pages 253-268
Verification of a Signature Architecture with HOL-Z....Pages 269-285
End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform....Pages 286-301
Formal Verification of Security Properties of Smart Card Embedded Source Code....Pages 302-317
A Formal Model of Addressing for Interoperating Networks....Pages 318-333
An Approach to Unfolding Asynchronous Communication Protocols....Pages 334-349
Semantics of BPEL4WS-Like Fault and Compensation Handling....Pages 350-365
On Some Galois Connection Based Abstractions for the Mu-Calculus....Pages 366-381
Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern....Pages 382-398
Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion....Pages 399-414
Synthesis of Distributed Processes from Scenario-Based Specifications....Pages 415-431
Verifying Scenario-Based Aspect Specifications....Pages 432-447
An MDA Approach Towards Integrating Formal and Informal Modeling Languages....Pages 448-464
Model-Checking of Specifications Integrating Processes, Data and Time....Pages 465-480
Automatic Symmetry Detection for Model Checking Using Computational Group Theory....Pages 481-496
On Partitioning and Symbolic Model Checking....Pages 497-511
Dynamic Component Substitutability Analysis....Pages 512-528
Floating-Point Verification....Pages 529-532
Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications....Pages 533-536
Model-Based Testing in Practice....Pages 537-541
Testing Concurrent Object-Oriented Systems with Spec Explorer....Pages 542-547
ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software....Pages 548-551
The Informal Nature of Systems Engineering....Pages 552-556
Back Matter....Pages -
