CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A Coverage Analysis for Safety Property Lists

Koen Claessen (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Conference on Formal Methods for Computer Aided Design (FMCAD), Austin, TX, NOV 11-14, 2007 (2007)
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2008-01-25. Senast ändrad 2013-08-05.
CPL Pubid: 67786

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur