基于k-定界的动态下推网络可达性分析

Research on k-delimited accessibility analysis for dynamic pushdown network

为了保证含有递归、动态创建线程并发系统的安全性,提出基于动态下推网络模型的形式化验证方法。该模型的可达性为不可判定,把动态下推网络转换为在k-定界下可达性可判定的下推网络,再将转换后的下推网络符号化。分析表明,该方法可使模型可达性成为可判定的,且缓解了模型状态空间爆炸的状态。

In order to ensure the security of concurrent system which contains recursion and dynamic creating threads, the formal verification method based on dynamic pushdown network model is proposed. The accessibility of this model is undeeidable. The dynamic pushdown network is transformed into the accessibility which can be decidable under the k-delimited condition. And then the transformed pushdown network is symbolized. The analysis shows that the method makes the accessibility of the model decidable and greatly optimizes the problem of model state space explosion,