Advanced Software Analysis and Verification

Source Code Verification:

The normal assessment methods for source code fall into two distinct categories: Dynamic Analysis (e.g. animation, testing) and Static Analysis. Dynamic Analysis works by exercising the code over a set of test conditions. It is based on engineering judgement: test conditions have to be chosen to maximise the likelihood that if the code behaves correctly for the test conditions, it will work when it encounters all other conditions. Static Analysis is based on logic: verification is by logical argument rather than execution. It can be applied with varying degrees of rigour, from code walkthroughs and inspections through to fully formal proof. MALPAS can be used to support both dynamic and static analyses, to any level of rigour, but it is most closely associated with Static Analysis. A realistic illustration of its capabilities is given in the companion document, “MALPAS – Advanced Software Analysis and Verification – Example Analysis”. In practice, dynamic and static analyses are complementary: testing can be used to check the assumptions in logical arguments and logical arguments can be used to check deficiencies in testing. Dynamic Analysis provides confidence that the code works reliably in foreseeable situations. It establishes that the software and hardware work together as planned, and provides some assurance that a compiler has not introduced unwanted errors. However, latent errors may emerge only on rare occasions and may be very difficult to trace. Furthermore, latent errors may be activated as a side-effect of maintenance.