TECHNICAL REPORT ARCHIVE


Classifying Properties: An Alternative to the Safety-Liveness Classification

TR-CIS-2000-03
Gleb Naumovich, Lori A. Clarke

pdf version of this paper

Abstract:
Traditionally, verification properties have been classified into safety and liveness properties. While this taxonomy has an attractive simplicity and is useful for identifying the appropriate analysis algorithm to use for checking a property, determining whether a property is safety, liveness, or neither can require significant mathematical insight on the part of the analyst. In this paper, we present an alternative property taxonomy. We argue that this taxonomy is a more natural classification of the kinds of questions that analysts want to ask. Moreover, most classes in our taxonomy have a known, direct mapping to the safety-liveness classification, and thus the appropriate analysis algorithm can be automatically determined.

Back to previous page