Abstract

This paper presents an approach to formally verify the detection capability of a system hang detector. To achieve this goal, an abstract formal model of a typical Linux system is created to thoroughly exercise all execution scenarios that may lead to hangs. The goal is to expose cases (i.e., hang scenarios) that escape detection. Our system model abstracts the basic hardware (e.g., timer, hardware counter) and software (e.g., processes/threads) components present in the Linux system. The model enables: (i) capturing behavior of these components so as to depict execution scenarios that lead to hangs, and (ii) evaluating hang detection coverage. Explicit-state model checking is applied to reason about system behavior and uncover hang scenarios that escape detection. The results indicate that the proposed framework allows identification of corner cases of hang scenarios that escape detection and provides valuable insight to developers for enhancing detection mechanisms.

Original languageEnglish (US)
Title of host publicationProceedings of the 27th IEEE International Symposium on Reliable Distributed Systems, SRDS 2008
Pages269-278
Number of pages10
DOIs
StatePublished - Dec 1 2008
Event27th IEEE International Symposium on Reliable Distributed Systems, SRDS 2008 - Napoli, Italy
Duration: Oct 6 2008Oct 8 2008

Publication series

NameProceedings of the IEEE Symposium on Reliable Distributed Systems
ISSN (Print)1060-9857

Other

Other27th IEEE International Symposium on Reliable Distributed Systems, SRDS 2008
Country/TerritoryItaly
CityNapoli
Period10/6/0810/8/08

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Formalizing system behavior for evaluating a system hang detector'. Together they form a unique fingerprint.

Cite this