Fme 2002: Formal Methods-Getting It Right : International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 2002 : Proceedings

by Eriksson, Lars-Henrik; Lindsay, Peter Alexander

• ISBN13: 9783540439288
• ISBN10: 3540439285
• Format: Paperback
• Copyright: 2002-08-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the international symposium Formal Methods Europe, FME 2002, held in Copenhagen, Denmark, in July 2002.The 31 revised full papers presented together with three invited contributions were carefully reviewed and selected from 95 submissions. All current aspects of formal methods are addressed, from foundational and methodological issues to advanced application in various fields.

Table of Contents

Little Engines of Proof	1	(20)
Natarajan Shankar
Automated Boundary Testing from Z and B	21	(20)
Bruno Legeard
Fabien Peureux
Mark Utting
Improvements in Coverability Analysis	41	(16)
Gil Ratsaby
Baruch Sterin
Shmuel Ur
Heuristic-Driven Test Case Selection from Formal Specifications A Case Study	57	(20)
Juan C. Burguillo-Rial
Manuel J. Fernandez-Iglesias
Francisco J. Gonzalez-Castano
Martin Llamas-Nistal
UniTesK Test Suite Architecture	77	(12)
Igor B. Bourdonov
Alexander S. Kossatchev
Victor V. Kuliamin
Alexander K. Petrenko
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited	89	(17)
David von Oheimb
Tobias Nipkow
Do Not Read This	106	(20)
Juan C. Bicarregui
Safeness of Make-Based Incremental Recompilation	126	(20)
Niels Jorgensen
An Algorithmic Approach to Design Exploration	146	(17)
Sharon Barner
Shoham Ben-David
Anna Gringauze
Baruch Sterin
Yaron Wolfsthal
Mechanical Abstraction of CSPZ Processes	163	(21)
Alexandre Mota
Paulo Borba
Augusto Sampaio
Verifying Erlang Code: A Resource Locker Case-Study	184	(20)
Thomas Arts
Clara Benac Earle
John Derrick
Towards an Integrated Model Checker for Railway Signalling Data	204	(20)
Michael Huber
Steve King
Correctness by Construction: Integrating Formality into a Commercial Development Process	224	(10)
Anthony Hall
Valloy -- Virtual Functions Meet a Relational Language	234	(18)
Darko Marinov
Sarfraz Khurshid
Verification Using Test Generation Techniques	252	(20)
Vlad Rusu
Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java	272	(18)
Nestor Catano
Marieke Huisman
Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods	290	(20)
Ludovic Casset
Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation	310	(20)
Michael Backes
Christian Jacobi
Birgit Pfitzmann
Interference Analysis for Dependable Systems Using Refinement and Abstraction	330	(20)
Claus Pahl
The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism	350	(20)
N. Henderson
S.E. Paynter
Timing Analysis of Assembler Code Control-Flow Paths	370	(20)
C. J. Fidge
Towards OCL/RT	390	(20)
Maria Victoria Cengarle
Alexander Knapp
On Combining Functional Verification and Performance Evaluation Using CADP	410	(20)
Hubert Garavel
Holger Hermanns
The Next 700 Synthesis Calculi	430	(1)
David Basin
Synthesizing Certified Code	431	(20)
Michael Whalen
Johann Schumann
Bernd Fischer
Refinement in Circus	451	(20)
Augusto Sampaio
Jim Woodcock
Ana Cavalcanti
Forward Simulation for Data Refinement of Classes	471	(20)
Ana Cavalcanti
David A. Naumann
A Formal Basis for a Program Compilation Proof Tool	491	(20)
Luke Wildman
Property Dependent Abstraction of Control Structure for Software Verification	511	(20)
Thomas Firley
Ursula Goltz
Closing Open SDL-Systems for Model Checking with DTSpin	531	(18)
Natalia Ioustinova
Natalia Sidorova
Martin Steffen
A Generalised Sweep-Line Method for Safety Properties	549	(19)
Lars Michael Kristensen
Thomas Mailund
Supplementing a UML Development Process with B	568	(19)
Helen Treharne
Semantic Web for Extending and Linking Formalisms	587	(20)
Jin Song Dong
Jing Sun
Hai Wang
A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels	607	(18)
Takaaki Umedu
Yoshiki Terashima
Keiichi Yasumoto
Akio Nakata
Teruo Higashino
Kenichi Taniguchi
Author Index	625