Integrated Formal Methods

1. Front Matter

   PDF

2. Contribution to a Rigorous Analysis of Web Application Frameworks

   • Egon Börger, Antonio Cisternino, Vincenzo Gervasi

   Pages 1-20

3. Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management

   • Muffy Calder, Michele Sevegnani

   Pages 21-23

4. Translating TLA⁺ to B for Validation with ProB

   • Dominik Hansen, Michael Leuschel

   Pages 24-38

5. Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands

   • Brijesh Dongol, Ian J. Hayes

   Pages 39-53

6. Safety and Line Capacity in Railways – An Approach in Timed CSP

   • Yoshinao Isobe, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach

   Pages 54-68

7. Refinement-Based Development of Timed Systems

   • Jesper Berthing, Pontus Boström, Kaisa Sere, Leonidas Tsiopoulos, Jüri Vain

   Pages 69-83

8. Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage Reports

   • Tim Blackmore, David Halliwell, Philip Barker, Kerstin Eder, Naresh Ramaram

   Pages 84-98

9. Model Checking as Static Analysis: Revisited

   • Fuyuan Zhang, Flemming Nielson, Hanne Riis Nielson

   Pages 99-112

10. Formal Verification of Compiler Transformations on Polychronous Equations

    • Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic, Loïc Besnard

    Pages 113-127

11. Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples

    • Herbert Rocha, Raimundo Barreto, Lucas Cordeiro, Arilo Dias Neto

    Pages 128-142

12. MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis

    • Fatemeh Kazemeyni, Einar Broch Johnsen, Olaf Owe, Ilangko Balasingham

    Pages 143-157

13. Mechanized Extraction of Topology Anti-patterns in Wireless Networks

    • Matthias Woehrle, Rena Bakhshi, Mohammad Reza Mousavi

    Pages 158-173

14. A Proof Framework for Concurrent Programs

    • Leonard Lensink, Sjaak Smetsers, Marko van Eekelen

    Pages 174-190

15. A UTP Semantics of pGCL as a Homogeneous Relation

    • Riccardo Bresciani, Andrew Butterfield

    Pages 191-205

16. Behaviour-Based Cheat Detection in Multiplayer Games with Event-B

    • HaiYun Tian, Phillip J. Brooke, Anne-Gwenn Bosser

    Pages 206-220

17. Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems

    • Denisa Diaconescu, Ioana Leustean, Luigia Petre, Kaisa Sere, Gheorghe Stefanescu

    Pages 221-236

18. Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B

    • Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis

    Pages 237-252

19. Partially-Supervised Plants: Embedding Control Requirements in Plant Components

    • Jasen Markovski, Dirk A. van Beek, Jos Baeten

    Pages 253-267

20. Early Fault Detection in Industry Using Models at Various Abstraction Levels

    • Jozef Hooman, Arjan J. Mooij, Hans van Wezep

    Pages 268-282

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.

• B-method
• compliance checking
• hybrid methods
• model checking
• runtime model generation
• algorithm analysis and problem complexity

• Department of Computer Science, University of Sheffield, Sheffield, UK

  John Derrick

• Consiglio Nazionale delle Ricerche, Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, Pisa, Italy

  Stefania Gnesi, Diego Latella

• Department of Computing, University of Surrey, Surrey, UK

  Helen Treharne

Policies and ethics