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 language | English (US) |
---|---|
Pages | 61-71 |
Number of pages | 11 |
DOIs | |
State | Published - 2000 |
Externally published | Yes |
Event | 3rd Workshop on Formal Methods in Software Practice (FMSP'00) - Portland, OR, USA Duration: Aug 24 2000 → Aug 25 2000 |
Conference
Conference | 3rd Workshop on Formal Methods in Software Practice (FMSP'00) |
---|---|
City | Portland, OR, USA |
Period | 8/24/00 → 8/25/00 |
ASJC Scopus subject areas
- General Computer Science