用形式化技术对JAVA程序进行逆向工程

《用形式化技术对JAVA程序进行逆向工程》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、论文摘要软件正确性的要求变得越来越明显，许多重大的、甚至致命的事故都源于软件的错误。另外，软件的维护工作是软件专家门所长期面对的问题。软件的平均寿命是10到15年，随着新结构的发展和程序方法、语占的改进，包括在软件方法、面向对象程序上形式化的应用，有必要对程序源代码进行逆向工程、再工程，以获得系统功能的提取及对程序的正确性的验证。形式化方法对于软件的发展，尤其是正向工程方面提供了许多益处。形式化方法的优势是形式化标记是精确的、可验证的、有利于自动处理。逆向工程是利用现存系统构造高水平的抽象表达，这方面最常用的就是形式化方法，即将源

2、代码进行形式化归约。本文描述的逆向工程中的形式化方法具体采用最强后件谓词转换技术SP及Houe理论中有关程序语义的部分正确性模型。以前我们也研究过最弱前件谓词转换WP用于理解形式化方法。这两种方法的不同之处在于SP可直接用于对源代码进行谓词转换而WP可用于构造形式化说明的参照。为了更好的说明这种方法，我们先对逆向工程及其相关概念给出了明确的定义。逆向工程是分析目标系统的过程，以便能确定系统的组件和它们之间的相互关系，并以另一种形式或者在更高的抽象级别上建立对系统的表示。正向工程是指软件开发的传统过程，这是为了区别于逆向工程而强调其

3、为正向的。对于逆向工程中的再文档和设计恢复技术也作了简单的说明。文中提出了“再工程=逆向工程+重构十正向工程”的再工程模型，使我们知道再工程一般包括一些形式的逆向工程，以得到更多关于系统的抽象描述。最后阐述了逆向工程的六大目标，及其在软件维护和软件再工程中的地位。通过对逆向工程和再工程等概念的介绍，我们可以明确本文描述的进行逆向工程的方法是适用于实现和设计级别的，也就是说它是一种适用于逆向工程初级阶段的方法。本文的研究重点是在如何用形式化方法来进行逆向工程。形式化方法是综合使用形式化规约语言的技术。形式化方法是有正确数学基础的方法

4、，它区别于结构化方法。形式化方法一般由语义模型，形式化语言，校验系统和支持工具四个基本部分组成。形式化方法可以被分为五大类，也就是基于模型的、基于网络的(图形的)、代数的、过程代数的和基于逻辑的形式化方法。而本文采用的是基于Hoare逻辑的逻辑形式化方法。Hoare逻辑提供了一种能说明程序和它的规约相一致的方式。虽然Hoare逻辑不能在很高的级别上说明一个系统，但是它在对系统进行低级别的说明上有独特的优点。这两个特征使Hoare逻辑成为逆向工程第一阶段最合适的方式。也就是说，可以用Hoare逻辑从源代码得到很低级别的抽象。本文提出

5、的方法主要是针对Java程序系统进行逆向工程的，文中对Java程序的基本语法结构应用最强后件语义定义了赋值语句规则、选择语句规则、循环语句规则、顺序语句规则，抽象匹配规则，建立了关于Java程序的最小公理系统。本文的形式化分析都是基于这个公理系统的。本文提出的方法综合使用了前端语法分析工具和形式化的技术。在具体的分析过程中，我们先通过前端工具对源代码进行词法、语法分析，通过得到的方法、类的视图软件工程师可以确定需要进一步分析的关键方法，便于软件工程师进一步对系统进行分析。最后本文描述一个实验性的工具JavaSpec，它对源代码进行

6、形式化规约生成，并通过抽象匹配规则得到更高级别的抽象，用于对目标系统进行分析。AbstractThedemandforsoftwarecorrectnessbecomesmoreevidentwhenaccidents，sometimesfatal，areduetosoftwareerrors。maintenancehaslongbeenaproblemfacedbysoftwareprofessionals,wheretheaverageageofsoftwareisbetween10to15yearsold.Withthede

7、velopmentofnewarchitecturesandimprovementsinprogrammingmethodsandlanguages,includingformalmethodsinsoftwaredevelopmentandobject-orientedprogramming,thereisastrongmotivationtoreverseengineerandre-engineerexistingcodeinordertopreservefunctionality.Formalmethodsinsoftwar

8、edevelopmentprovidemanybenefitsintheforwardengineeringaspectofsoftwaredevelopment.Oneoftheadvantagesofusingformalmethodsinso