Model checking conformance with scenario-based specifications

Abstract

Specifications that describe typical scenarios of operations have become common for software applications, using, for example, use-cases of UML. For a system to conform with such a specification, every execution sequence must be equivalent to one in which the specified scenarios occur sequentially, where we consider computations to be equivalent if they only differ in that independent operations may occur in a different order. A general framework is presented to check the conformance of systems with such specifications using model checking. Given a model and additional information including a description of the scenarios and of the operations' independence, an augmented model using a transducer and temporal logic assertions for it are automatically defined and model checked. In the augmentation, a small window with part of the history of operations is added to the state variables. New transitions are defined that exchange the order of independent operations, and that identify and remove completed scenarios. If the model checker proves all the generated assertions, every computation is equivalent to some sequence of the specified scenarios. A new technique is presented that allows proving equivalence with a small fixed-size window in the presence of unbounded out-of-order of operations from unrelated scenarios. This key technique is based on the prediction of events, and the use of anti-events to guarantee that predicted events will actually occur. A prototype implementation based on Cadence SMV is described. © Springer-Verlag Berlin Heidelberg 2003.