Diagram Refinements for the Design of Reactive Systems

Dominique Cansell, Dominique Méry, Stephan Merz

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 and a diagram, 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.

Available as:  gzip'ed Postscript

Reference

@Article{cansell:refinement,
  author =  {Dominique Cansell and Dominique M{\'e}ry and Stephan Merz},
  title =   {Diagram Refinements for the Design of Reactive Systems},
  journal = {Journal of Universal Computer Science},
  year =    2001,
  volume =  7,
  number =  2,
  pages =   {159--174}
}