Diagram Refinements for the Design of Reactive Systems
Дата
Авторы
Cansell,Dominique
Mery,Dominique
Merz,Stephan
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
refinement , abstraction , verification , temporal logic , TLA , diagrams