【硕士论文】形式化技术在逆向工程中的应用研究.pdf

《【硕士论文】形式化技术在逆向工程中的应用研究.pdf》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、学校代号10536分类号至旦31l学密囊沙罗哥歹文乎硕士学位论文号Q三Q22Q垒曼级——形式化技术在逆向工程中的应用研究学位申请人姓名当笪塑培养单位计算机与通信工程学院导师姓名及职称何锫教授学科专业计算机应用技术研究方向筮鲑王猩论文提交日期2006年3月10曰摘要随着计算机技术的飞速发展，产生了越来越多的遗产系统，对这些系统进行维护和升级是软件工程师们经常要面对的问题。要对遗产系统进行维护和再工程，就需要用逆向工程技术对当前系统的结构和行为进行理解。作为软件工程中的～种新技术，逆向工程能够分析目标系统，确定系统的组件和它们之间的相互关系，并以另一种形式或者

2、在更高的抽象级别上建立对系统的表示，从而帮助维护人员理解并重构软件系统。形式化方法对于软件的发展，尤其是正向工程方面提供了许多好处。形式化方法的一个优点是它的表示是精确的、可验证的，这样有助于使用自动化的处理。一种利用形式化方法优点的方式就是通过对现有程序代码进行逆向工程来得到形式化规约。本文描述的逆向工程中的形式化方法采用最强后置条件谓词转换技术和Hoare理论中有关程序语义的部分正确性模型，研究的重点是利用形式化技术和非形式化技术对程序代码进行逆向工程，以支持软件理解和维护。针对C程序的基本语法结构定义了赋值语句规则、选择语句规则、循环语句规则、顺序语

3、句规则和函数调用规则，建立了一个最小的公理系统。介绍了以C—Minus语言(自定义的一种简化的C语言子集)为实例进行逆向工程的过程。在进行逆向分析的过程中，首先对源程序进行词法语法分析生成语法树，从结构化源程序中提取源程序的模板信息，并把模板信息用一个二叉树表示，之后按照设计的二叉树遍历算法，把二叉树转化为PAD(ProblemAnalysisDiagram)图，用以描述程序的结构，并作为可视化的人工理解辅助工具，便于我们从中方便的选出源代码的关键部分。在结构化分析的基础上，对关键性的源代码文件进行扫描，对每条语句进行分析，根据C程序语句中各种基本结构的最

4、强后置条件形式化语义，对每条语句按照相应的规则进行转换，得到程序的形式规约。关键词：逆向工程；形式化方法；最强后置条件；PAD图；形式规约AbstractWiththerapiddevelopmentofcomputertechnology，moreandmorelegacysystemswereproduced．Maintainingandupgradingthesesystemshavelongbeenaproblemfacedbysoftwareengineers．Itisnecessarytousethetechnologyofreverseeng

5、ineeringtoanalysisthestructureandbehaviorofthecurrentsysteminordertomaintainandre—engineeringthelegacysystbms．Reverseengineeringistheprocessofanalyzingasystemtoidentifythecomponentsandtheirrelationshipsandcreaterepresentationsofthesysteminanotherformoratahigherlevelofabstraction，w

6、hichcanhelpengineersunderstandandreconstructsoftwaresystem．Formalmethodsinsoftwaredevelopmentprovidemanybenefitsintheforwardengineering．Abenefitofformalmethodsisthattheirnotationsarewell—definedandthus，areamenabletoautomatedprocessing．Onemethodforintroducingformalmethods，andtheref

7、oretakingadvantageofthebenefitsofformalmethodsisthroughthereverseengineeringofexistingprogramcodeintoformalspecifications．Thispaperdescribesanapproachtoreverseengineeringbasedontheformalsemanticsofthestrongestpostconditionpredicatetransformer，andthepartialcorrectnessmodelofprogram

8、semanticsintroducedbyHoare．Themai