Fault origin adjudication

10 years 1 months ago
Fault origin adjudication
When a program P fails to satisfy a requirement R supposedly ensured by a detailed speci cation S that was used to implement P, there is a question about whether the problem arises in S or in P. We call this determination fault origin adjudication and illustrate its signi cance in various software engineering contexts. The primary contribution of this paper is a framework for formal fault origin adjudication for network protocols using the NS/2 simulator and the SPIN model checker. We describe our architecture and illustrate its use in a case study involving a standard speci cation for packet radio routing.
Karthikeyan Bhargavan, Carl A. Gunter, Davor Obrad
Added 01 Aug 2010
Updated 01 Aug 2010
Type Conference
Year 2000
Where FMSP
Authors Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic
Comments (0)