JUCS - Journal of Universal Computer Science 7(2): 159-174, doi: 10.3217/jucs-007-02-0159
Diagram Refinements for the Design of Reactive Systems
expand article infoDominique Cansell‡, Dominique Mery§, Stephan Merz|
‡ Université de Metz & LORIA, France§ Université Henri Poincare & LORIA, France| Institut für Informatik, Universität München, Germany

Corresponding author: Dominique Cansell ( cansell@loria.fr )

© Dominique Cansell, Dominique Mery, Stephan Merz.
This article is freely available under the J.UCS Open Content License.
Citation: Cansell D, Mery D, Merz S (2001) Diagram Refinements for the Design of Reactive Systems. JUCS - Journal of Universal Computer Science 7(2): 159-174. https://doi.org/10.3217/jucs-007-02-0159
Open Access
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
refinement, abstraction, verification, temporal logic, TLA, diagrams