Assume-guarantee supervisor for concurrent systems
Mohammad Zulkernine, Rudolph E. Seviora · 2005
Despite rigorous use of model checking, testing, and other technological innovations in software development there exists faults which elude those detection efforts and do not surface until the software is operational. These faults may lead to serious software failures (deviation of actual behavior from the desired one). Existing software failure detectors for concurrent systems are not compositional, and hence suffer from the state explosion problem. We present a compositional approach for automatic failure detection of concurrent programs specified as a collection of communi-cating finite state machines. The failure detector described in this paper is called assume-guarantee supervisor. The su-pervisor simultaneously observes the input/output and sta-ble states of the target system, interprets the specification, and reports the discrepancies between these two as failures. We formalize an assume-guarantee paradigm for supervi-sion, and provide a generic failure detection algorithm. We also describe the architecture and operation of a failure de-tection tool which employs the above model. This tool can be employed for online software failure detection in the op-erational stage of a system. 1