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.

• Type: Conference
• Year: 2000
• Where: FMSP
• Authors: Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic
• Keywords: Determination Fault Origin, Fault Origin Adjudication, FMSP 2000, Formal Methods, Speci Cation