|Title:||Model Checking Reductions to Convenient Computations
|Authors:||Marcelo Glusman and Shmuel Katz
|Abstract:||In many applications, such as database serializability, shared memory sequential consistency, or as part of a layered proof of other properties, it is natural to ask whether every computation of a system can be reduced to one of the particular computations considered `convenient' due to their perceived regularity. Computations related by the reductions described here differ only in having independent operations occur in a different order. A general framework is presented in which, given a model and additional information including a description of the convenient computations 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 bounded history queue is added to the state variables, and new transitions are defined that exchange the order of independent operations and identify prefixes of convenient computations. If the model checking proves all the generated assertions, every computation can be reduced to a convenient one. Events can be `predicted', and `anti-events' are used to guarantee that they actually occur. This new technique allows treating many cases of unbounded out-of-order of operations relative to the convenient computations. A prototype implementation based on Cadence SMV is described.|
|Copyright||The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information|
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2003/CS/CS-2003-01), rather than to the URL of the PDF or PS files directly. The latter URLs may change without notice.
To the list of the CS technical reports of 2003
To the main CS technical reports page
Computer science department, Technion