支持抽象解释的静态分析方法的形式化体系研究

Research on Static Analysis Formalism Supporting Abstract Interpretation

在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。

In safety critical domain,software safety assurance becomes a widely concerned issue.Static program analysis is an effective method for automating program validation.Static analysis is an efficient formal method for the use of verification of non functional safety-critical properties.CPA(Configurable Program Analysis)is a formalism for static analysis.It intends to describe the analysis phrase in static analysis by a general formal framework.This paper aimed at formally modeling the analysis phrase in abstract interpretation with the formalism CPA.We illuminated the rules of transformation from source code to the formalism of configurable program analysis.This paper provided a way to automatically verify the software correctness in safety critical domain and provided a feasible solution for static analysis tool based on abstract interpretation.