Integrated Formal Methods: 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings (Lecture Notes in Computer Science, 4591)

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 Title Page Preface Organization Table of Contents Verifying Temporal Properties of CommUnity Designs Introduction CommUnity Designs Component Composition Semantics of Architectures Semantics for Abstract CommUnity Designs Verifying Temporal Properties of Designs The SMV System Translating CommUnity Designs into SMV Modularising the Verification Through Morphisms Some Sample Properties Conclusions References Precise Scenarios – A Customer-Friendly Foundation for Formal Specifications Introduction Ordering Problem and State Space NewOrder InvoiceOrder CancelOrder EnterStock Validation Underspecification Overspecification Nondeterminism Testing Tool Support Required Conclusions References Automated Verification of Security Policies in Mobile Code Introduction Related Work Formal Semantics of Mobile Programs Mobile Programs The ComputationalModel Specifying Security Policies of Mobile Programs Security and Projection A Model Checking Framework for Verification of Security Policies Experimental Results Conclusion References Slicing Concurrent Real-Time System Specifications for Verification Introduction CSP-OZ-DC Slicing Control Flow Graph Program Dependence Graph Backward Slice Reduced Specification Correctness Conclusion References Slotted-Circus A UTP-Family of Reactive Theories Introduction \Circus\ and Slotted-\Circus UTP: General Principles Structure and Focus Syntax Generic Slot-Theory Derived Types and Operators Healthiness Conditions Reactive Healthiness CSP Healthiness Slotted Semantics Laws 5.2 Links Instantiating Slotted-\Circus Multiset History Instantiation Example Circus Process Related Work Future Work Conclusions References Bug Hunting with False Negatives Introduction The Specification Framework \altl\ with Data (\eALTL\/) Abstraction of Systems and Properties Abstraction of a System Abstraction of $eALTL$ Formulae Classification of Counterexamples Bug Hunting with False Negatives Constructing a Violation Pattern Looking for a Concrete Counterexample Correctness of the Framework Implementation Conclusion References Behavioural Specifications from Class Models Introduction UML Class Diagrams and OCL State Diagrams The $Booster$ Language The Generation of State Diagrams Abstraction Transitions States Validation and Verification A Worked Example An Example Specification Generation Discussion Related Work Further Work References Inheriting Laws for Processes with States Introduction Unifying Theories of Programming A Meta-theory of Predicative Modelling Set-Theoretic Predicate Calculus 3.2 Predicate Functions Semantic Inheritance Basic Models Partially Correct Relational Model Sequential Specifications CSP-Z Specifications The Model CSP Commands and Action System Law Inheritance Parallelism as Conjunction 5.5 Binary Compositions 5.6 CSP Conclusions and Future Work References Probabilistic Timed Behavior Trees Introduction Preliminaries on Behavior Trees Behavior Trees Timed Behavior Trees Semantics of Timed Behavior Trees Operational Semantics Concurrent Timed Behavior Trees Probabilistic Timed Behavior Trees Semantics of Probabilistic Timed Behavior Trees Semantics of Concurrent Probabilistic Timed Behavior Trees Model Checking Probabilistic Timed Behavior Trees Case Study 1 - Lamp Example Case Study 2 - Viking Example Related Work Conclusion and Future Work References Guiding the Correction of Parameterized Specifications Introduction Correction of a B Machine Translation into Why Language Parameter Instantiation Sort-Based Instantiation Incremental Instantiation Reaching the Counter-Example Using the ProB Model-Checker Symbolic Animation Efficiency Keynotes on the BZ-Testing-Tools Animator Interpreting the Reachability Result Related Work Conclusion and Future Work References Proving Linearizability Via Non-atomic Refinement Introduction An Abstract and a Concrete Stack Background Generalised Non-atomic Refinement Example Linearizability Conclusion References Lifting General Correctness into PartialCorrectness is $ok$ Introduction Preliminaries General Correctness and Abstract Commands The Interactive Era Abstract Commands Normal Form of an Abstract Command Indeterminate Assignment General Correctness and UTP Prescriptions $versus$ Predicate Transformers Pseudo-prescriptions Lifting a Computation Lifting Abstract Commands An Example Conclusion References Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters Introduction Illustration CSP-OZ-DC: A High-Level Specification Language Timing Parameters in COD Operational Semantics of COD Specifications Translation of COD Specifications into PEA PEA with Timing Parameters Simplifications of PEA Verification of COD Specifications Translation of PEA to TCS Verification of TCS Efficient Reasoning in Complex Theories: Locality Example: The RBC Case Study Conclusions References Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks Introduction The LMAC Protocol Timed Automata Models and Properties Model Decomposition Properties Simplification Results Safety and Reachability Properties Liveness Properties Conclusion References Finding State Solutions to Temporal Logic Queries Introduction Background Query Checking State Solutions to Queries SolvingMinterm Query Checking Implementation Exactness of Minterm Approximation Approximations Case Study Conclusions References Qualitative Probabilistic Modelling in Event-B Introduction The Event-B Modelling Notation Machines Machine Refinement Qualitative Probabilistic Event-B Almost Certain Convergence in Event-B The Rejected Alternatives Preliminary Study of Refinement Example: Contention Resolution in the Firewire Protocol Overview of the Firewire Protocol Event-B Model of the Contention Problem Attempting Nondeterministic Contention Resolution Probabilistic Contention Resolution Soundness Conclusion References Verifying Smart Card Applications: An ASM Approach Introduction Concepts of the Application Model Modeling the Agents The Attacker The ASM The Attacker Regular Agents Graphical Notation An Electronic Wallet Internal State of the Agents The Terminal Proving Properties Main Security Property Verification Technique Protocols and Their Expected Functionalities Related Work Conclusion References Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function Introduction Preliminaries HOL Theorem Prover Verifying Probabilistic Algorithms in HOL Formalization of the Standard Uniform Distribution Formal Specification of Standard Uniform Random Variable Formal Verification of Standard Uniform Random Variable Formalization of the Cumulative Distribution Function Formal Specification of CDF Formal Verification of CDF Properties CDF Properties and Probabilistic Analysis Determining Interval Probabilities Representing PMF in Terms of the CDF Representing PDF in Terms of the CDF Illustrative Example Formal Specification of the Continuous Uniform Distribution CDF Verification of the Continuous Uniform Random Variable Verification of Probabilistic Properties Related Work Conclusions References UTP Semantics for Web Services Introduction A Model for Fault Handling Programming Language Link with the Design Calculus Rollback Compensation Conclusion References Combining Mobility with State Introduction Notation Combining B Machines and $\pi$ Processes Mediators Example Identifying and Discharging Assertions Underlying Semantics Discussion Related Work Future Work References Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System Introduction Overview of the Mondex Electronic Purse System The OTS/CafeOBJ Method CafeOBJ: Algebraic Specification Language Observational Transition Systems (OTSs) Specification of OTSs in CafeOBJ Verification of Invariants of OTSs Formalization of the Mondex System Basic Data Types OTS Model and Its CafeOBJ Specification Verification of the Mondex System Formal Definitions of the Properties Verification of the Properties Falsification of the Mondex System Maude Specification of the Mondex System Falsification of the Mondex System Related Work Conclusion References Capturing Conflict and Confusion in CSP Introduction PetriNets Graphical Representation Formal Representation Concurrency, Conflict and Confusion Purity Enabled Transitions and Pre- and Post-Conditions Interference Concurrency Conflict Confusion CSP Syntax Semantics Refinement Capturing Marked Petri Nets as CSP Processes Capturing Places Eliminating Interference Capturing Nets Testing for Conflict The \emphControl Processes The \emph{AfterCheck} Processes Processes $\LHS$ and $\RHS$ The Test Testing for Conflict-Decreasing Confusion Processes LHS and RHS The\emphControl Processes The \emph{AfterCheck Processes} The Test Testing for Conflict-Increasing Confusion Processes LHS and RHS The \emphControl Processes The \emph{AfterCheck} Processes The Test Discussion References A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems Introduction ActionSystems Semantics Probabilistic Action Systems Semantics Continuous Action Systems Semantics Combining Probabilistic and Continuous Action Systems The Probabilistic Steam Boiler Extracting the Non-probabilistic Behaviour Introducing Time and Continuous Behaviour Refining the Real-Time Steam Boiler Conclusion References Decomposing Integrated Specifications for Verification Introduction A Specification in CSP-OZ Semantics of CSP-OZ: Labelled Kripke Structures Syntax and Semantics of Requirements: LTL-X Decomposition Decomposing a CSP-OZ Specification: Weak Slicing Decomposition of the Example Verification Verification of the Example Conclusion References Validating Z Specifications Using the ProB Animator and Model Checker Introduction Specifications in Z A Brief Description of Z Some Differences Between Z and B Translating Z to B Architecture and the proz Compiler Identifying Components of the Specification Translating Initialisation and Operations from Z to B New Constructs and Operators NewTypes Schema Types Free Types Case study Route Calculation Network Protocol Discussion, Related and Future Work References Verification of Multi-agent Negotiations Using the Alloy Analyzer Introduction Brief Overview of Alloy Subject System Details Property Examples Derived from Requirements Experiment Design Choice of the Analyzed System Relation Between Protocol FSMs, Task Structures, Offers and Visitations Details of the Task Allocation Problem in the Chosen Design Alloy Specification for the Negotiation Model Alloy Specification for the Properties Specification Difficulties Conclusions and Future Work References Integrated Static Analysis for Linux Device Driver Verification Introduction On Programs, Specifications, Hazards and Specification Implementations Adapting SDV Extending SLIC to SLICx Verification Engine CBMC An Operating System Model for Linux Example: RCU-API Checking BeyondSDV Memory Preemption Simulation (PS) Sound Locking (AL) Complete Locking (LO) Race Conditions (UA) Additional Techniques Empirical Results Modularity Issues Results on Real Drivers Related Work Summary References Integrating Verification, Testing, and Learning for Cryptographic Protocols Introduction Models Syntax of IOSTS Semantics of IOSTS Parallel Product Verification, Testing, and Learning Expressing Security Properties Using Observers The Intruder Modelling the Protocol, Performing the Verification Learning by Testing Our Approach Conclusion and Future Work References Translating FSP into LOTOS and Networks of Automata Introduction FSP, LOTOS, and EXP Preliminary Definitions Environment Expressions Translation of a Label Hiding or Renaming Translating FSP Sequential Processes into LOTOS Sequence of Labels Sequential Processes Translating FSP Composite Processes into EXP Tool and Validation Application Concluding Remarks References Common Semantics for Use Cases and Task Models Introduction Background Use Case Models Task Models Use Cases vs. Task Models: A Comparison Related Work Semantics for Use Cases and Task Models Intermediate Semantic Domain for Use Cases Intermediate Semantic Domain for Task Models Common Semantic Domain Based on Sets of Posets Satisfiability Between Use Cases and Task Models Conclusion and Future Work References Unifying Theories of Objects Introduction Designs in Unifying Theories of Programming Design Frame and Compilation Notation Operational Reduction Rule Notation The Object Calculi Abadi–Cardelli Untyped Object Calculus Core Object Calculus (\langid{O}{c}-Calculus) Heap-Extended Object Calculus (\langid{O}{ch}-Calculus) The Operand Stack Model (\langid{U}{sh}) of the\langid{O}{ch}-Calculus Literal Value Programs Modelling Object Values and Method Definitions Command Expressions Method Updates and Field Assignments Method Invocation Modelling the Heap Operations Consistency of the Operand Stack Model Scalar Value Operations Method Invocation Fresh Heap Locations Conclusions and Related Work Related Work On-Going Work References Non-interference Properties for Data-Type Reduction of Communicating Systems Introduction Dynamic Communication Systems Analysis of Dynamic Communication Systems Data-Type Reduction for DCS Refining Data-Type Reduction by Process Counting Related Work Conclusion References Co-simulation of Distributed Embedded Real-Time Control Systems Introduction Current State of Practice in Academia and Industry Modeling and Analysis of Embedded Control Systems Plant Modeling Controller Description Tool Support Reconciled Operational Semantics Syntax Operational Semantics Concluding Remarks References Author Index