Fault origin adjudication

Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

Research output: Contribution to conferencePaper

Abstract

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)
Pages61-71
Number of pages11
DOIs
StatePublished - Jan 1 2000
Externally publishedYes
Event3rd Workshop on Formal Methods in Software Practice (FMSP'00) - Portland, OR, USA
Duration: Aug 24 2000Aug 25 2000

Conference

Conference3rd Workshop on Formal Methods in Software Practice (FMSP'00)
CityPortland, OR, USA
Period8/24/008/25/00

ASJC Scopus subject areas

  • Computer Science(all)

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

  • Cite this

    Bhargavan, K., Gunter, C. A., & Obradovic, D. (2000). Fault origin adjudication. 61-71. Paper presented at 3rd Workshop on Formal Methods in Software Practice (FMSP'00), Portland, OR, USA, . https://doi.org/10.1145/349360.351132