Fault origin adjudication

Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

Research output: Contribution to conferencePaperpeer-review


When a program P fails to satisfy a requirement R supposedly ensured by a detailed specification 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 significance 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 simulator and the SPIN model checker. We describe our architecture and illustrate its use in a case study involving a standard specification for packet radio routing.

Original languageEnglish (US)
Number of pages11
StatePublished - 2000
Externally publishedYes
Event3rd Workshop on Formal Methods in Software Practice (FMSP'00) - Portland, OR, USA
Duration: Aug 24 2000Aug 25 2000


Conference3rd Workshop on Formal Methods in Software Practice (FMSP'00)
CityPortland, OR, USA

ASJC Scopus subject areas

  • General Computer Science


Dive into the research topics of 'Fault origin adjudication'. Together they form a unique fingerprint.

Cite this