PUSH-BUTTON VERIFICATION AND DEBUGGING FOR COBOL-BASED FINANCIAL SYSTEMS

摘要

Formal Methods have been adopted successfully by industriesrnfor which safety is paramount or the cost of errorsrnexorbitant. Even so, Formal Methods are virtuallyrnunknown in the domain of Financial Services, despiternpersistent and economically significant software qualityrnchallenges. The Babel prototype is introduced to demonstraternan innovative approach to encapsulating powerfulrnFormal Methods into automated Push-Button verificationrnfor COBOL-based Financial Services software.rnThe essential adoption barrier for Financial Services isrnthe knowledge of Logic and Computation Theory requiredrnfor their successful use. Babel’s Push-Buttonrnapproach eliminates Formal Methods’ educational prerequisites,rnsimplifies their use, and integrates seamlesslyrninto the existing software development task structurernand tools. Babel’s Human-Computer Interaction advancesrnare based upon complete and correct static analysis,rnwhich in turn are based upon the thesis that the corernsystems in Financial Services can be implemented on arnsimpler computational model than core systems in otherrnindustries. Babel implements the static analysis andrnautomated verification using symbolic execution, arnmodified semantic tableau, and subsumption reasoning.rnVerification tasks are defined in a point-and click-queryrnuser interface, in which a visual source trace capabilityrnseamlessly links verification failures to root causes inrnprogram source.