基于CPA的抽象解释分析方法研究
    点此下载全文
引用本文:张 弛,黄志球,丁泽文,刘林武.基于CPA的抽象解释分析方法研究[J].计算技术与自动化,2017,(3):118-123
摘要点击次数: 996
全文下载次数: 0
作者单位
张 弛,黄志球,丁泽文,刘林武 (南京航空航天大学 计算机科学与技术学院江苏 南京 211106) 
中文摘要:安全关键领域中,如何保证软件安全性已经成为了一个广受关注的重要课题。确保程序中没有运行时错误,对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象,是验证运行时错误最合适的形式化方法之一。可配置程序分析(configurable program analysis,CPA)是一种适合多种静态分析方法的通用分析框架。本文使用CPA对抽象解释分析方法进行建模,给出了使用基于CPA的抽象解释方法验证程序中的运行时错误的验证流程,并用实例说明该验证方法的有效性。为程序中运行时错误的自动化分析和验证提供了一种可行方案。
中文关键词:可配置程序分析  抽象解释  静态分析  运行时错误验证
 
Research on Abstract Interpretation Based on Configurable Program Analysis
Abstract:How to ensure software safety has become an important subject in safety critical domain.Ensuring the absence of run-time errors in the program is very important for the safety of the software.The program semantics was abstracted by the static analysis method based on abstract interpretation,and it is one of the most appropriate formal methods for validating run-time errors.Configurable program analysis is a general analytical framework for a variety of static analysis methods.The CPA is used to model the abstraction analysis method,and the validation process of using CPA-based abstract interpretation method to verify the run-time errors in the program is given.Then the effectiveness of the method is illustrated by an example.This provides a feasible solution for the automatic analysis and verification of run-time errors in the program.
keywords:configurable program analysis  abstract interpretation  static analysis  run-time error verification 
查看全文   查看/发表评论   下载pdf阅读器