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.
Author(s): Thai Son Hoang, Hironobu Kuruma, David Basin, Jean-Raymond Abrial (auth.), Michael Leuschel, Heike Wehrheim (eds.)
Series: Lecture Notes in Computer Science 5423 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 367
Tags: Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Software Engineering; Programming Techniques
Front Matter....Pages -
Developing Topology Discovery in Event-B....Pages 1-19
Decomposition Structures for Event-B....Pages 20-38
Taming the Unbounded for Hardware Synthesis....Pages 39-39
Verifying UML/OCL Operation Contracts....Pages 40-55
Property Specifications for Workflow Modelling....Pages 56-71
Formal Verification Based on Guided Random Walks....Pages 72-87
Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format....Pages 88-102
Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B....Pages 103-117
CSP with Hierarchical State....Pages 118-135
Predicate Abstraction in a Program Logic Calculus....Pages 136-150
Mechanised Translation of Control Law Diagrams into Circus ....Pages 151-166
Realizability of Choreographies Using Process Algebra Encodings....Pages 167-182
Modelling Divergence in Relational Concurrent Refinement....Pages 183-199
SAL-Based Symbolic Scheduling in Time-Triggered Networks....Pages 200-214
Incremental Reasoning for Multiple Inheritance....Pages 215-230
Model Checking LTL Formulae in RAISE with FDR....Pages 231-245
An Introduction to Grammar Convergence....Pages 246-260
Application of Graph Transformation in Verification of Dynamic Systems....Pages 261-276
Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays....Pages 277-291
Challenges in the Specification of Full Contracts....Pages 292-306
Partial Order Reduction for State/Event LTL....Pages 307-321
Dynamic Path Reduction for Software Model Checking....Pages 322-336
Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions....Pages 337-351
Decompositional Petri Net Reductions....Pages 352-366
Back Matter....Pages -
