Automating and evaluating assume-guarantee reasoning.

摘要

Software systems are taking on an increasingly important role in society and are being used in critical applications where their failure could result in human casualties or substantial economic loss. Thus, it is important to validate software systems to ensure their quality. One technique for validating software systems is finite-state verification, in which a finite model of a system is analyzed to ensure that it satisfies a property that specifies a desired system behavior. Unfortunately, the cost of finite-state verification can be exponential in the size of the system being analyzed.; Compositional analysis is a "divide-and-conquer" approach to verification that aims to reduce the cost of verification. One proposed compositional technique is assume-guarantee reasoning. With this technique a system is decomposed into subsystems and these subsystems are analyzed individually. By composing the results of these analyses, it can be determined whether or not a system satisfies a property. Because each subsystem is smaller than the whole system, analyzing each subsystem individually may reduce the overall cost of verification. Often the behavior of a subsystem is dependent on the subsystems with which it interacts, and thus it is usually necessary to provide assumptions about the environment in which a subsystem executes. Because developing assumptions has been a difficult manual task, the evaluation of assume-guarantee reasoning has been limited.; In this thesis we present an algorithm that automatically learns assumptions. Using this algorithm, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. Using two different verifiers, we considered all two-way decompositions for a set of systems and properties. By increasing the number of repeated tasks in these systems, we evaluated the decompositions as they were scaled. We found that in only a few cases can assume-guarantee reasoning verify properties on larger systems than monolithic verification can and in these cases the systems that can be analyzed are only a few sizes larger. Although these results are discouraging, they provide insight about research directions that should be pursued and highlight the importance of experimental evaluation.