Abstract: This paper presents two points of improvements for model checking temporal safety properties of program: more efficient model checking algorithm is proposed, which can simplify the checking process and reduce the time cost by extending the state machine model with each function. Alias analysis is used to determine the dataflow dependency between safety operations, which makes the checking process more accurate. Experimental results show that the method can work more efficiently and exactly.

Key words: temporal safety property, model checking, alias analysis

摘要： 针对程序时序安全属性模型检测技术改进模型检测算法，使安全漏洞状态机以函数为单位进行扩展，简化程序模型检测过程，以提高检测效率。在检测过程中加入别名分析，考虑安全操作之间的数据流依赖关系，以提高检测的准确性。实验结果表明，改进后的方法比原检测方法具有更高的效率和准确性。

关键词: 时序安全属性, 模型检测, 别名分析

CLC Number: 

• TP311