Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007. Proceedings

Nazareno Aguirre, Germán Regis, Tom Maibaum (auth.), Jim Davies, Jeremy Gibbons (eds.)3540732098, 9783540732099

This book constitutes the refereed proceedings of the 6th International Conference on Integrated Formal Methods, IFM 2007, held in Oxford, UK in July 2007.

The 32 revised full papers presented together with 1 invited paper were carefully reviewed and selected from 85 submissions. The papers address all aspects of formal methods integration, including of a process of analysis or design application of formal methods to analysis or design, extension of one method, based upon the inclusion of ideas or concepts from others, informal or semi-formal modelling languages, tools, or techniques, and semantic integration or practical application.

---

Table of contents :
Front Matter….Pages –
Verifying Temporal Properties of CommUnity Designs….Pages 1-20
Precise Scenarios – A Customer-Friendly Foundation for Formal Specifications….Pages 21-36
Automated Verification of Security Policies in Mobile Code….Pages 37-53
Slicing Concurrent Real-Time System Specifications for Verification….Pages 54-74
Slotted-Circus….Pages 75-97
Bug Hunting with False Negatives….Pages 98-117
Behavioural Specifications from Class Models….Pages 118-137
Inheriting Laws for Processes with States….Pages 138-155
Probabilistic Timed Behavior Trees….Pages 156-175
Guiding the Correction of Parameterized Specifications….Pages 176-194
Proving Linearizability Via Non-atomic Refinement….Pages 195-214
Lifting General Correctness into Partial Correctness is ok ….Pages 215-232
Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters….Pages 233-252
Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks….Pages 253-272
Finding State Solutions to Temporal Logic Queries….Pages 273-292
Qualitative Probabilistic Modelling in Event-B….Pages 293-312
Verifying Smart Card Applications: An ASM Approach….Pages 313-332
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function….Pages 333-352
UTP Semantics for Web Services….Pages 353-372
Combining Mobility with State….Pages 373-392
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System….Pages 393-412
Capturing Conflict and Confusion in CSP….Pages 413-438
A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems….Pages 439-458
Decomposing Integrated Specifications for Verification….Pages 459-479
Validating Z Specifications Using the ProB Animator and Model Checker….Pages 480-500
Verification of Multi-agent Negotiations Using the Alloy Analyzer….Pages 501-517
Integrated Static Analysis for Linux Device Driver Verification….Pages 518-537
Integrating Verification, Testing, and Learning for Cryptographic Protocols….Pages 538-557
Translating FSP into LOTOS and Networks of Automata….Pages 558-578
Common Semantics for Use Cases and Task Models….Pages 579-598
Unifying Theories of Objects….Pages 599-618
Non-interference Properties for Data-Type Reduction of Communicating Systems….Pages 619-638
Co-simulation of Distributed Embedded Real-Time Control Systems….Pages 639-658
Back Matter….Pages –