Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 7 / Issue 2

available in:   PDF (138 kB) PS (215 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-007-02-0159


Diagram Refinements for the Design of Reactive Systems

Dominique Cansell (Université de Metz & LORIA, France)

Dominique Mery (Université Henri Poincare & LORIA, France)

Stephan Merz (Institut für Informatik, Universität München, Germany)

Abstract: We define a class of predicate diagrams that represent abstractions of - possibly infinite-state - reactive systems. Our diagrams support the verification of safety as well as liveness properties. Non-temporal proof obligations establish the correspondence between the original specification, whereas model checking can be used to verify behavioral properties. We define a notion of refinement between diagrams that is intended to justify the top_down development of systems within the framework of diagrams. The method is illustrated by a number of mutual-exclusion algorithms.

Keywords: TLA, abstraction, diagrams, refinement, temporal logic, verification

Categories: D.2.2, D.2.4, F.3.1