Formal Methods and Software Engineering
7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005, Proceedings
Kung-Kiu Lau & Richard Banach (editors)
Contents
Realising the Benefits of Formal Methods . Hall, Anthony - pages 1-4
A Compositional Framework for Service Interaction Patterns and Interaction Flows - Barros, Alistair (et al.) - pages 5-35
An Evidential Tool Bus - Rushby, John - pages 36-36
Derivation of UML Class Diagrams as Static Views of Formal B Developments - Idani, Akram (et al.) - pages 37-51
29 New Unclarities in the Semantics of UML 2.0 State Machines - Fecher, Harald (et al.) - pages 52-65
The Semantics and Tool Support of OZTA - Dong, Jin Song (et al.) - pages 66-80
An Abstract Model for Process Mediation - Altenhofen, Michael (et al.) - pages 81-95
How Symbolic Animation Can Help Designing an Efficient Formal Model - Bouquet, Fabrice (et al.) - pages 96-110
A Theory of Secure Control Flow - Abadi, Martín (et al.) - pages 111-124
Game Semantics Model for Security Protocols - Debbabi, Mourad (et al.) - pages 125-140
Towards Dynamically Communicating Abstract Machines in the B Method - Aguirre, Nazareno (et al.) - pages 141-155
Sweep-Line Analysis of TCP Connection Management - Gallasch, Guy Edward (et al.) - pages 156-172
2/3 Alternating Simulation Between Interface Automata - Wen, Yanjun (et al.) - pages 173-187
Formal Model-Driven Development of Communicating Systems - Laibinis, Linas (et al.) - pages 188-203
Jahuel: A Formal Framework for Software Synthesis - Assayad, I. (et al.) - pages 204-218
Modelling and Refinement of an On-Chip Communication Architecture - Plosila, Juha (et al.) - pages 219-234
Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics - Sobeih, Ahmed (et al.) - pages 235-250
Adaptive Random Testing by Bisection with Restriction - Mayer, Johannes - pages 251-263
Testing Real-Time Multi Input-Output Systems - Briones, Laura Brandán (et al.) - pages 264-279
Formal Verification of a Memory Model for C-Like Imperative Languages - Blazy, Sandrine (et al.) - pages 280-299
Symbolic Verification of Distributed Real-Time Systems with Complex Synchronizations - Wang, Farn - pages 300-314
An Improved Rule for While Loops in Deductive Program Verification - Beckert, Bernhard (et al.) - pages 315-329
Using Stålmarck’s Algorithm to Prove Inequalities - Cook, Byron (et al.) - pages 330-344
Automatic Refinement Checking for B - Leuschel, Michael (et al.) - pages 345-359
Slicing an Integrated Formal Method for Verification - Brückner, Ingo (et al.) - pages 360-374
A Static Communication Elimination Algorithm for Distributed System Verification - Babot, Francesc (et al.) - pages 375-389
Incremental Verification of Owicki/Gries Proof Outlines Using PVS - Mooij, Arjan J. (et al.) - pages 390-404
Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry - Brandt, Jens (et al.) - pages 405-420
An Automated Approach to Specification-Based Program Inspection - Liu, Shaoying (et al.) - pages 421-434
Visualizing and Simulating Semantic Web Services Ontologies - Sun, Jun (et al.) - pages 435-449
A Model-to-Implementation Mapping Tool for Automated Model-Based GUI Testing - Paiva, Ana C. R. (et al.) - pages 450-464
ClawZ: Cost-Effective Formal Verification for Control Systems - Adams, M. M. (et al.) - pages 465-479
SVG Web Environment for Z Specification Language - Sun, Jing (et al.) - pages 480-494
Springer, Lecture Notes in Computer Science #3785, Paperback, english, 494 pages