Applying Abstract Interpretation to Verify EN-50128 Software Safety Requirements

Like other contemporary safety standards EN-50128 requires 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 hazards are violations of resource bounds, especially stack overflows and deadline violations, as well as run-time errors and data races. They can cause erroneous and erratic program behavior, invalidate separation mechanisms in mixed-criticality software, and even trigger software crashes. Classical software verification methods like code review and testing with measurements cannot really guarantee the absence of errors. Abstract interpretation is a formal method for static program analysis which supports formal soundness proofs (it can be proven that no error is missed) and which scales. This article gives an overview of abstract interpretation and its application to compute safe worst-case execution time and stack bounds, and to find all potential run-time errors, and data races. We discuss the tool qualification of abstract interpretation-based static analyzers and describe their contribution with respect to EN-50128 compliant verification processes. We also illustrate their integration in the development process and report on practical experience.