Colloquium Details
Reasoning About Large Systems in a Compositional Way
| Author: | Dimitra Giannakopoulou NASA / Ames |
|---|---|
| Date: | August 23, 2001 |
| Time: | 16:00 |
| Location: | 220 Deschutes |
Abstract
Model checking is a highly automated technique for verifying properties of hardware or software systems. When provided with a formal description of a system's behavior and a required property, the model checker exhaustively explores all the states of the system and returns one of the following results:
- a yes answer, meaning the property is satisfied by the system;
- a counterexample illustrating how the system could violate the property.
More often than not, however, the model checker runs out of memory for any system of realistic size. This problem is known as "state explosion", which refers to the exponential relation between the state space of the system and the components of the state. Various techniques have been proposed to address this problem including abstraction, symbolic state representation, and compositionality.
Compositionality is recognized as the most promising attack to state explosion. It advocates a "divide-and-conquer" approach to verification, and comes in two forms. "Compositional verification" involves reasoning about properties of a system in terms of properties of its components. Compositional minimization exploits the hierarchical structure of a system to incrementally generate and check its behavior. In this talk, we will discuss these two forms of compositionality, and focus on the main benefits and problems that they introduce. We will demonstrate some initial results on applying such techniques to the Remote Agent, a case study that the ASE group at NASA Ames has already analyzed in a non-compositional setting.