Automatic Verification on the Large

Farn Wang and Pao-Ann Hsiung
Institute of Information Science
Academia Sinica, Taipei, Taiwan.
( International Symposium on High-Assurance Systems Engineering (HASE'98) , Washington, D.C., U.S.A., November 13-14, 1998.)


An automatic verification method from a high-level resource-management standpoint is presented. Various manipulators can be incorporated in the method to construct, refine, reduce, and model-check state space representation. Proper combinations of manipulators can then be picked strategically by users or computers for less resource (time and space) consumption. An algorithm based on group theory to pick a manipulator combination is presented. Verification sessions are conducted to illustrate our idea.