A Coverage Analysis for Safety Property Lists
A Coverage Analysis for Safety Property Lists
复制标题
安全属性列表的覆盖率分析
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Koen Claessen
中科院分区：
文献类型：
--
作者：
Koen Claessen
我们提供了可用于基于物业的验证的覆盖范围分析。该分析有助于确定“被遗忘的案件”；分析属性列表的方案不会在某个时间点限制某个输出。然后可以手动调查这些方案，可能导致添加了新的，以前被遗忘的属性。由于通常存在不应该指定输出的情况，我们还提供了较较高的注释属性的方法，以控制应该不受限制的情况。与较早提出的类似分析存在两个主要区别：提出的分析是与设计无关的，并且在故意和无意间指定的行为之间明确区分。
We present a coverage analysis that can be used in property-based verification. The analysis helps identifying "forgotten cases"; scenarios where the property list under analysis does not constrain a certain output at a certain point in time. These scenarios can then be manually investigated, possibly leading to new, previously forgotten properties being added. As there often exist cases in which outputs are not supposed to be specified, we also provide means for the specificier to annotate properties in order to control what cases are supposed to be underconstrained. Two main differences with earlier proposed similar analyses exist: The presented analysis is design-independent, and it makes an explicit distinction between intentionally and unintentionally underspecified behavior.