Integrated Formal Methods: 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings (Lecture Notes in Computer Science, 7321)

Annotation This book constitutes the refereed proceedings of the 9th International Conference on Integrated Formal Methods, IFM 2012, held Pisa, Italy, in June 2012. The 20 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 59 submissions. The papers cover the spectrum of integrated formal methods, ranging from formal and semiformal notations, semantics, proof frameworks, refinement, verification, timed systems, as well as tools and case studies Front Matter....Pages - Contribution to a Rigorous Analysis of Web Application Frameworks....Pages 1-20 Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management....Pages 21-23 Translating TLA + to B for Validation with ProB ....Pages 24-38 Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands....Pages 39-53 Safety and Line Capacity in Railways – An Approach in Timed CSP....Pages 54-68 Refinement-Based Development of Timed Systems....Pages 69-83 Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage Reports....Pages 84-98 Model Checking as Static Analysis: Revisited....Pages 99-112 Formal Verification of Compiler Transformations on Polychronous Equations....Pages 113-127 Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples....Pages 128-142 MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis....Pages 143-157 Mechanized Extraction of Topology Anti-patterns in Wireless Networks....Pages 158-173 A Proof Framework for Concurrent Programs....Pages 174-190 A UTP Semantics of pGCL as a Homogeneous Relation....Pages 191-205 Behaviour-Based Cheat Detection in Multiplayer Games with Event-B....Pages 206-220 Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems....Pages 221-236 Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B....Pages 237-252 Partially-Supervised Plants: Embedding Control Requirements in Plant Components....Pages 253-267 Early Fault Detection in Industry Using Models at Various Abstraction Levels....Pages 268-282 PE -KeY: A Partial Evaluator for Java Programs....Pages 283-295 Specification-Driven Unit Test Generation for Java Generic Classes....Pages 296-311 Specifying UML Protocol State Machines in Alloy....Pages 312-326 Patterns for a Log-Based Strengthening of Declarative Compliance Models....Pages 327-342 A Formal Interactive Verification Environment for the Plan Execution Interchange Language....Pages 343-357 Back Matter....Pages - This Festschrift published in honor of Vladimir Lifschitz on the occasion of his 65th birthday presents 39 articles by colleagues from all over the world with whom Vladimir Lifschitz had cooperation in various respects.