Advertisement

© 2009

Integrated Formal Methods

7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009. Proceedings

  • Michael Leuschel
  • Heike Wehrheim
Conference proceedings IFM 2009

Part of the Lecture Notes in Computer Science book series (LNCS, volume 5423)

Table of contents

  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
      PDF

  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
    17. Challenges in the Specification of Full Contracts
      Gordon J. Pace, Gerardo Schneider
      Pages 292-306
    18. Partial Order Reduction for State/Event LTL
      Nikola Beneš, Lubos Brim, Ivana Černá, Jiri Sochor, Pavlina Vařeková, Barbora Zimmerova
      Pages 307-321
    19. Dynamic Path Reduction for Software Model Checking
      Zijiang Yang, Bashar Al-Rawi, Karem Sakallah, Xiaowan Huang, Scott Smolka, Radu Grosu
      Pages 322-336
    20. Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions
      Jérémy Milhau, Benoît Fraikin, Marc Frappier
      Pages 337-351
    21. Decompositional Petri Net Reductions
      Astrid Rakow
      Pages 352-366
  4. Back Matter
    PDF

About these proceedings

Introduction

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.

Keywords

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

Editors and affiliations

  • Michael Leuschel
    • 1
  • Heike Wehrheim
    • 2
  1. 1.Institut für InformatikHeinrich-Heine-Universität DüsseldorfDüsseldorfGermany
  2. 2.Fakultät für Elektrotechnik, Informatik und MathematikUniversität PaderbornPaderbornGermany

Bibliographic information

Industry Sectors
Automotive
Electronics
IT & Software
Telecommunications
Aerospace
Engineering