A Coverage Analysis for Safety Property Lists

Abstract

We present a coverage analysis that can be used in\nproperty-based verification. The analysis helps identifying ”forgotten\ncases”; scenarios where the property list under analysis\ndoes not constrain a certain output at a certain point in time.\nThese scenarios can then be manually investigated, possibly leading\nto new, previously forgotten properties being added. As there\noften exist cases in which outputs are not supposed to be specified,\nwe also provide means for the specificier to annotate properties in\norder to control what cases are supposed to be underconstrained.\nTwo main differences with earlier proposed similar analyses\nexist: The presented analysis is design-independent, and it makes\nan explicit distinction between intentionally and unintentionally\nunderspecified behavior.