Formal Methods and Software Engineering: 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, October 29 – November 1, 2013, Proceedings

Description

This book constitutes the refereed proceedings of the 15th International Conference on Formal Engineering Methods, ICFEM 2013, held in Queenstown, New Zealand, in October/November 2013. The 28 revised full papers together with 2 keynote speeches presented were carefully reviewed and selected from 88 submissions. The topics covered are abstraction and refinement, formal specification and modeling, program analysis, software verification, formal methods for software safety, security, reliability and dependability, tool development, integration and experiments involving verified systems, formal methods used in certifying products under international standards, and formal model-based development and code generation. Front Matter....Pages - Lattices of Information for Security: Deterministic, Demonic, Probabilistic....Pages 1-3 Algebraic Laws for Process Subtyping....Pages 4-19 Boundness Issues in CCSL Specifications....Pages 20-35 Mining Dataflow Sensitive Specifications....Pages 36-52 A Proof Slicing Framework for Program Verification....Pages 53-69 Formally Verified System Initialisation....Pages 70-85 Verifying an Aircraft Proximity Characterization Method in Coq....Pages 86-101 Assisting Specification Refinement by Random Testing....Pages 102-114 Generation of Checking Sequences Using Identification Sets....Pages 115-130 The Circus Testing Theory Revisited in Isabelle/HOL....Pages 131-147 A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification....Pages 148-164 Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts....Pages 165-181 Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction....Pages 182-198 A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems....Pages 199-214 A UTP Semantics for Communicating Processes with Shared Variables....Pages 215-230 Verification of Static and Dynamic Barrier Synchronization Using Bounded Permissions....Pages 231-248 Formal Models of SysML Blocks....Pages 249-264 Towards a Process Algebra Framework for Supporting Behavioural Consistency and Requirements Traceability in SysML....Pages 265-280 Translation from Workflow Nets to MSVL....Pages 281-296 Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems....Pages 297-312 Verification of Functional and Non-functional Requirements of Web Service Composition....Pages 313-328 vTRUST: A Formal Modeling and Verification Framework for Virtualization Systems....Pages 329-346 Formal Kinematic Analysis of the Two-Link Planar Manipulator....Pages 347-362 Formal Modelling of Resilient Data Storage in Cloud....Pages 363-379 Linking Operational Semantics and Algebraic Semantics for Wireless Networks....Pages 380-396 Automated Specification Discovery via User-Defined Predicates....Pages 397-414 Path-Sensitive Data Flow Analysis Simplified....Pages 415-430 Reconstructing Paths for Reachable Code....Pages 431-446 The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software....Pages 447-463 Back Matter....Pages -