形式化技術(shù)在逆向工程中的應(yīng)用研究.pdf

1、學(xué)校代號(hào)10536分類(lèi)號(hào)至旦31l學(xué)密囊沙羅哥歹文乎碩士學(xué)位論文號(hào)Q三Q22Q壘曼級(jí)——形式化技術(shù)在逆向工程中的應(yīng)用研究學(xué)位申請(qǐng)人姓名當(dāng)笪塑培養(yǎng)單位計(jì)算機(jī)與通信工程學(xué)院導(dǎo)師姓名及職稱(chēng)何锫教授學(xué)科專(zhuān)業(yè)計(jì)算機(jī)應(yīng)用技術(shù)研究方向筮鮭王猩論文提交日期2006年3月10曰AbstractWiththerapiddevelopmentofcomputertechnology，moreandmorelegacysystemswereproducedMa

2、intainingandupgradingthesesystemshavelongbeenaproblemfacedbysoftwareengineersItisnecessarytousethetechnologyofreverseengineeringtoanalysisthestructureandbehaviorofthecurrentsysteminordertomaintainandre—engineeringthelega

3、cysystbmsReverseengineeringistheprocessofanalyzingasystemtoidentifythecomponentsandtheirrelationshipsandcreaterepresentationsofthesysteminanotherformoratahigherlevelofabstraction，whichcanhelpengineersunderstandandreconst

4、ructsoftwaresystemFormalmethodsinsoftwaredevelopmentprovidemanybenefitsintheforwardengineeringAbenefitofformalmethodsisthattheirnotationsarewell—definedandthus，areamenabletoautomatedprocessingOnemethodforintroducingforma

5、lmethods，andthereforetakingadvantageofthebenefitsofformalmethodsisthroughthereverseengineeringofexistingprogramcodeintoformalspecificationsThispaperdescribesanapproachteverseengineeringbasedontheformalsemanticsofthestron

6、gestpostconditionpredicatetransformer，andthepartialcorrectnessmodelofprogramsemanticsintroducedbyHoareThemainpointofourinvestigationishowtouseinformalandformalmethodsforreverseengineeringTheapproachprovidedbythisthesisis

7、mainlytoprocesstheCprogramsystemforreverseengineeringInthethesiswedefinedtheassignmentrule，alternationrule，iterationrule，sequenceruleandfunctionruleaccordingtothebasicsyntaxstructuresofCprogramsandsetupanaxiomsystemofCpr

8、ogramsTheprocessofreverseengineeringisintroducedthroughaninstance，C—Minus(asimplifiedClanguage)Inreverseengineering，theabstractsyntaxtreeisgeneratedbylexicalanalysisandsyntaxanalysisfromsourcecodeThetemplateinformationis

9、extractedfromstructuredsourcecode，whichisrepresentedbyabinarytreeThenthebinarytreeistranslatedintothePAD(ProblemAnalysisDiagram)accordingtothedesignedalgorithmAfterstructuredanalysis，thestatementsofkeysourcecodewillbesca

10、nned，andeachstatementwillbetranslatedintoformalspecificationaccordingtothestrongestposteonditionsemanticsofthebasicstructureKeyWords：Reverseengineering；Formalmethod；Strongestpostcondition；Problemanalysisdiagram；Formalspe