Integrated Formal Methods

1. Front Matter

   PDF

2. Invited Talks

   1. Developing Topology Discovery in Event-B

      • Thai Son Hoang, Hironobu Kuruma, David Basin, Jean-Raymond Abrial

      Pages 1-19

   2. Decomposition Structures for Event-B

      • Michael Butler

      Pages 20-38

   3. Taming the Unbounded for Hardware Synthesis

      • Byron Cook

      Pages 39-39

3. Contributed Papers

   1. Verifying UML/OCL Operation Contracts

      • Jordi Cabot, Robert Clarisó, Daniel Riera

      Pages 40-55

   2. Property Specifications for Workflow Modelling

      • Peter Y. H. Wong, Jeremy Gibbons

      Pages 56-71

   3. Formal Verification Based on Guided Random Walks

      • Thang H. Bui, Albert Nymeyer

      Pages 72-87

   4. Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format

      • Jan Stöcker, Frédéric Lang, Hubert Garavel

      Pages 88-102

   5. Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B

      • Steve Schneider, Helen Treharne

      Pages 103-117

   6. CSP with Hierarchical State

      • Robert Colvin, Ian J. Hayes

      Pages 118-135

   7. Predicate Abstraction in a Program Logic Calculus

      • Benjamin Weiß

      Pages 136-150

   8. Mechanised Translation of Control Law Diagrams into Circus

      • Frank Zeyda, Ana Cavalcanti

      Pages 151-166

   9. Realizability of Choreographies Using Process Algebra Encodings

      • Gwen Salaün, Tevfik Bultan

      Pages 167-182

   10. Modelling Divergence in Relational Concurrent Refinement

       • Eerke Boiten, John Derrick

       Pages 183-199

   11. SAL-Based Symbolic Scheduling in Time-Triggered Networks

       • Sebastian Voss, Maria Sorea, Klaus Echtle

       Pages 200-214

   12. Incremental Reasoning for Multiple Inheritance

       • Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen

       Pages 215-230

   13. Model Checking LTL Formulae in RAISE with FDR

       • Abigail Parisaca Vargas, Ana G. Garis, S. Lizeth Tapia Tarifa, Chris George

       Pages 231-245

   14. An Introduction to Grammar Convergence

       • Ralf Lämmel, Vadim Zaytsev

       Pages 246-260

   15. Application of Graph Transformation in Verification of Dynamic Systems

       • Zarrin Langari, Richard Trefler

       Pages 261-276

   16. Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays

       • Osman Hasan, Naeem Abbasi, Sofiène Tahar

       Pages 277-291

This book constitutes the refereed proceedings of the 7th International Conference on Integrated Formal Methods, IFM 2009, held in Düsseldorf, Germany in February 2009. The 21 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 55 submissions. The papers address the whole spectrum of integrated formal methods, ranging from formal and semiformal modelling notations, semantics, verification, refinement, model transformations to type systems, logics, tools and case studies.

• Event-B
• Model Checking
• Petri
• automata
• case studies
• component systems
• constraint satisfaction
• data refinement
• divergence
• formal semantics
• formal verification
• logic
• petri net
• semantics
• verification

• Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, Düsseldorf, Germany

  Michael Leuschel

• Fakultät für Elektrotechnik, Informatik und Mathematik, Universität Paderborn, Paderborn, Germany

  Heike Wehrheim

Policies and ethics