FM 2005: Formal Methods : International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings / edited by John Fitzgerald, Ian J. Hayes.

Format:

Book

Contributor:

Fitzgerald, John, 1965- editor.

Hayes, Ian J., editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Programming and software engineering ; SL 2, 3582.

Programming and Software Engineering ; 3582

Language:

English

Subjects (All):

Software engineering.

Computer logic.

Programming languages (Electronic computers).

Computer programming.

Logic, Symbolic and mathematical.

Management information systems.

Computer science.

Software Engineering.

Logics and Meanings of Programs.

Programming Languages, Compilers, Interpreters.

Programming Techniques.

Mathematical Logic and Formal Languages.

Management of Computing and Information Systems.

Local Subjects:

Software Engineering.

Logics and Meanings of Programs.

Programming Languages, Compilers, Interpreters.

Programming Techniques.

Mathematical Logic and Formal Languages.

Management of Computing and Information Systems.

Physical Description:

1 online resource (XIV, 558 pages).

Edition:

First edition 2005.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2005.

System Details:

text file PDF

Summary:

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).

Contents:

Keynote Talks

Formal Aids for the Growth of Software Systems

Formal Methods and Testing: Hypotheses, and Correctness Approximations

The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions

Object Orientation

Modular Verification of Static Class Invariants

Decoupling in Object Orientation

Controlling Object Allocation Using Creation Guards

Symbolic Animation of JML Specifications

Resource Analysis and Verification

Certified Memory Usage Analysis

Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs

Formally Defining and Verifying Master/Slave Speculative Parallelization

Timing and Testing

Systematic Implementation of Real-Time Models

Timing Tolerances in Safety-Critical Software

Timed Testing with TorX

Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems

CSP, B and Circus

Adding Conflict and Confusion to CSP

Combining CSP and B for Specification and Property Verification

Operational Semantics for Model Checking Circus

Control Law Diagrams in Circus

Security

Verification of a Signature Architecture with HOL-Z

End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform

Formal Verification of Security Properties of Smart Card Embedded Source Code

Networks and Processes

A Formal Model of Addressing for Interoperating Networks

An Approach to Unfolding Asynchronous Communication Protocols

Semantics of BPEL4WS-Like Fault and Compensation Handling

Abstraction, Retrenchment and Rewriting

On Some Galois Connection Based Abstractions for the Mu-Calculus

Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern

Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion

Scenarios and Modeling Languages

Synthesis of Distributed Processes from Scenario-Based Specifications

Verifying Scenario-Based Aspect Specifications

An MDA Approach Towards Integrating Formal and Informal Modeling Languages

Model Checking

Model-Checking of Specifications Integrating Processes, Data and Time

Automatic Symmetry Detection for Model Checking Using Computational Group Theory

On Partitioning and Symbolic Model Checking

Dynamic Component Substitutability Analysis

Industry Day: Abstracts of Invited Talks

Floating-Point Verification

Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications

Model-Based Testing in Practice

Testing Concurrent Object-Oriented Systems with Spec Explorer

ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software

The Informal Nature of Systems Engineering.

Other Format:

Printed edition:

ISBN:

978-3-540-31714-2

9783540317142

Access Restriction:

Restricted for use by site license.