S.P.C. Bucuvalas, A.M. Bader, T.D. Nelson, and R. Barnhart (USA)
Verification and Validation, Formal Methods, COBOL, and Tools
Formal Methods have been adopted successfully by in dustries for which safety is paramount or the cost of er rors exorbitant. Even so, Formal Methods are virtually unknown in the domain of Financial Services, despite persistent and economically significant software quality challenges. The Babel prototype is introduced to dem onstrate an innovative approach to encapsulating power ful Formal Methods into automated Push-Button verifi cation for COBOL-based Financial Services software. The essential adoption barrier for Financial Services is the knowledge of Logic and Computation Theory re quired for their successful use. Babel’s Push-Button approach eliminates Formal Methods’ educational pre requisites, simplifies their use, and integrates seamlessly into the existing software development task structure and tools. Babel’s Human-Computer Interaction ad vances are based upon complete and correct static analy sis, which in turn are based upon the thesis that the core systems in Financial Services can be implemented on a simpler computational model than core systems in other industries. Babel implements the static analysis and automated verification using symbolic execution, a modified semantic tableau, and subsumption reasoning. Verification tasks are defined in a point-and click-query user interface, in which a visual source trace capability seamlessly links verification failures to root causes in program source.
Important Links:
Go Back
