Formal Method Tools: Proving the Absence of Critical Errors by Abstract Interpretation

摘要

Contemporary safety standards require to identify potential functional and non-functional hazards, and to demonstrate that the software does not violate the relevant safety goals. Examples of safety-relevant non-functional program properties are resource usage - in particular worst-case execution time and stack usage - and absence of run-time errors. Such non-functional errors are hard to address by classical software validation methods. Code review and testing with measurements typically cause significant effort but cannot guarantee the absence of errors. A technique which can prove the absence of such errors is Abstract Interpretation, a mathematically rigorous formal methodology for static program analysis. Abstract interpretation enables the soundness of an analysis to be proven: the results are valid for all program runs with all inputs and provide full data and control coverage. Nowadays, abstract interpretation-based static analysers become widely used and define the state-of-the-art technology for validating non-functional program properties.