Interated Formal Methods

by Davies, Jim; Gibbons, Jeremy

• ISBN13: 9783540732099
• ISBN10: 3540732098
• Format: Paperback
• Copyright: 2007-09-03
• Publisher: Springer-Verlag New York Inc

Summary

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

Verifying temporal properties of CommUnity designs	p. 1
Precise scenarios - a customer-friendly foundation for formal specifications	p. 21
Automated verification of security policies in mobile code	p. 37
Slicing concurrent real-time system specications for verification	p. 54
Slotted-circus : a UTP-family of reactive theories	p. 75
Bug hunting with false negatives	p. 98
Behavioural specifications from class models	p. 118
Inheriting laws for processes with states	p. 138
Probabilistic timed behavior trees	p. 156
Guiding the correction of parameterized specifications	p. 176
Proving linearizability via non-atomic refinement	p. 195
Lifting general correctness into partial correctness is ok	p. 215
Verifying CSP-OZ-DC specifications with complex data types and timing parameters	p. 233
Modelling and verification of the LMAC protocol for wireless sensor networks	p. 253
Finding state solutions to temporal logic queries	p. 273
Qualitative probabilistic modelling in event-B	p. 293
Verifying smart card applications : an ASM approach	p. 313
Verification of probabilistic properties in HOL using the cumulative distribution function	p. 333
UTP semantics for Web services	p. 353
Combining mobility with state	p. 373
Algebraic approaches to formal analysis of the Mondex electronic purse system	p. 393
Capturing conflict and confusion in CSP	p. 413
A stepwise development process for reasoning about the reliability of real-time systems	p. 439
Decomposing integrated specifications for verification	p. 459
Validating Z specifications using the ProB animator and model checker	p. 480
Verification of multi-agent negotiations using the alloy analyzer	p. 501
Integrated static analysis for Linux device driver verification	p. 518
Integrating verification, testing, and learning for cryptographic protocols	p. 538
Translating FSP into LOTOS and networks of automata	p. 558
Common semantics for use cases and task models	p. 579
Unifying theories of objects	p. 599
Non-interference properties for data-type reduction of communicating systems	p. 619
Co-simulation of distributed embedded real-time control systems	p. 639
Table of Contents provided by Blackwell. All Rights Reserved.