Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005. Proceedings

✍ Scribed by Anthony Hall (auth.), Kung-Kiu Lau, Richard Banach (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2005
• Tongue: English
• Leaves: 507
• Series: Lecture Notes in Computer Science 3785 : Programming and Software Engineering
• Edition: 1
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 7th International Conference on Formal Engineering Methods, ICFEM 2005, held in Manchester, UK in November 2005.

The 30 revised full papers presented together with 3 invited contributions were carefully reviewed and selected from 74 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on specification, modelling, security, communication, development, testing, verification, and tools.

✦ Table of Contents

Front Matter....Pages -
Realising the Benefits of Formal Methods....Pages 1-4
A Compositional Framework for Service Interaction Patterns and Interaction Flows....Pages 5-35
An Evidential Tool Bus....Pages 36-36
Derivation of UML Class Diagrams as Static Views of Formal B Developments....Pages 37-51
29 New Unclarities in the Semantics of UML 2.0 State Machines....Pages 52-65
The Semantics and Tool Support of OZTA....Pages 66-80
An Abstract Model for Process Mediation....Pages 81-95
How Symbolic Animation Can Help Designing an Efficient Formal Model....Pages 96-110
A Theory of Secure Control Flow....Pages 111-124
Game Semantics Model for Security Protocols....Pages 125-140
Towards Dynamically Communicating Abstract Machines in the B Method....Pages 141-155
Sweep-Line Analysis of TCP Connection Management....Pages 156-172
2/3 Alternating Simulation Between Interface Automata....Pages 173-187
Formal Model-Driven Development of Communicating Systems....Pages 188-203
Jahuel : A Formal Framework for Software Synthesis....Pages 204-218
Modelling and Refinement of an On-Chip Communication Architecture....Pages 219-234
Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics....Pages 235-250
Adaptive Random Testing by Bisection with Restriction....Pages 251-263
Testing Real-Time Multi Input-Output Systems....Pages 264-279
Formal Verification of a Memory Model for C -Like Imperative Languages....Pages 280-299
Symbolic Verification of Distributed Real-Time Systems with Complex Synchronizations....Pages 300-314
An Improved Rule for While Loops in Deductive Program Verification....Pages 315-329
Using Stålmarck’s Algorithm to Prove Inequalities....Pages 330-344
Automatic Refinement Checking for B....Pages 345-359
Slicing an Integrated Formal Method for Verification....Pages 360-374
A Static Communication Elimination Algorithm for Distributed System Verification....Pages 375-389
Incremental Verification of Owicki/Gries Proof Outlines Using PVS....Pages 390-404
Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry....Pages 405-420
An Automated Approach to Specification-Based Program Inspection....Pages 421-434
Visualizing and Simulating Semantic Web Services Ontologies....Pages 435-449
A Model-to-Implementation Mapping Tool for Automated Model-Based GUI Testing....Pages 450-464
ClawZ: Cost-Effective Formal Verification for Control Systems....Pages 465-479
SVG Web Environment for Z Specification Language....Pages 480-494
Back Matter....Pages -

✦ Subjects

Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters