College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||Proving Nondeterministically Specified Safety Properties Using Progress Measures|
|Authors: ||Klarlund, Nils|
Schneider, Fred B.
|Keywords: ||computer science|
|Issue Date: ||May-1991|
|Publisher: ||Cornell University|
|Abstract: ||Using the notion of progress measures, we discuss verification methods for proving that a program satisfies a property specified by an automaton having finite nondeterminism. Such automata can express any safety property. Previous methods, which can be derived from the method presented here, either rely on transforming the program or are not to complete. In contrast, our ND progress measures describe a homomorphism from the unaltered program to a canonical specification automaton and constitute a complete verification method. The canonical specification automaton is obtained from the classical subset construction and a new subset construction, called historization.|
|Appears in Collections:||Computer Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.