并发系统模型检测中的状态约减算法

State Reduction in the Model Checking of Concurrent Systems

组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题。对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状态爆炸几率和提高验证效率。借助假定-保证(Assume-Guarantee)算法有效性定理和组合可达性分析(CRA)算法安全性验证定理,证明该验证算法的有效性。通过采用通信系统演算(CCS)描述的任务模型为例证,证明上述算法比传统CRA算法更有效。

The compositional reachability analysis （CRA） is hotspot of research in behavior analysis of concurrent systems. Traditional techniques, however, are often stymied by the state explosion problem. To cope with the problem, a new verification method, naming ABSR （Assume Based State-Reduction）, is proposed. Its efficiency is significantly improved and the complexity of the verification is decreased because the redundant states to be checked are discarded with automatically generated assumptions. Our ABSR method is described in CCS （Calculus of Communicating System）, and its validity is proved. A typical concurrent system, called task scheduler is deeply studied as a real case; initial experiment results show that our method is practicable.