FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings

Front Cover
John Fitzgerald, Ian J. Hayes
Springer Science & Business Media, Jul 4, 2005 - Computers - 558 pages
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).
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Formal Aids for the Growth of Software Systems
1
Hypotheses and Correctness Approximations
2
Using Formal Methods to Analyse Software Related Failures in Space Missions
9
Modular Verification of Static Class Invariants
26
Decoupling in Object Orientation
43
Controlling Object Allocation Using Creation Guards
59
Symbolic Animation of JML Specifications
75
Certified Memory Usage Analysis
91
A Formal Model of Addressing for Interoperating Networks
318
An Approach to Unfolding Asynchronous Communication Protocols
334
Semantics of BPEL4WSLike Fault and Compensation Handling
350
On Some Galois Connection Based Abstractions for the MuCalculus
366
Finite Sequence Numbers and the Tower Pattern
382
Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion
399
Synthesis of Distributed Processes from ScenarioBased Specifications
415
Verifying ScenarioBased Aspect Specifications
432

Compositional Specification and Analysis of CostBased Properties in Probabilistic Programs
107
Formally Defining and Verifying MasterSlave Speculative Parallelization
123
Systematic Implementation of RealTime Models
139
Timing Tolerances in SafetyCritical Software
157
Timed Testing with TorX
173
Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems
189
Adding Conflict and Confusion to CSP
205
Combining CSP and B for Specification and Property Verification
221
Operational Semantics for Model Checking Circus
237
Control Law Diagrams in Circus
253
Verification of a Signature Architecture with HOLZ
269
EndtoEnd Integrated Security and Performance Analysis on the DEGAS Choreographer Platform
286
Formal Verification of Security Properties of Smart Card Embedded Source Code
302
An MDA Approach Towards Integrating Formal and Informal Modeling Languages
448
ModelChecking of Specifications Integrating Processes Data and Time
465
Automatic Symmetry Detection for Model Checking Using Computational Group Theory
481
On Partitioning and Symbolic Model Checking
497
Dynamic Component Substitutability Analysis
512
FloatingPoint Verification
529
Model Checking for Advanced Automotive Applications
533
ModelBased Testing in Practice
537
Testing Concurrent ObjectOriented Systems with Spec Explorer
542
Costs and Benefits of Applying Formal Methods to Industrial Control Software
548
The Informal Nature of Systems Engineering
552
Author Index
557
Copyright

Other editions - View all

Common terms and phrases