Combining Testing and Proof to Gain High Assurance in Software: a Case Study

Dynamic software test methods are generally easy to use, but the results only apply to the specific input values tested. Static analysis produces results which are more general, but can require more effort to perform. There are potential benefits in combining both types of techniques because the results obtained can be more general than standalone dynamic testing but less resource-intensive than standalone static analysis. This paper presents a specific example of this approach applied to the verification of continuous monotonic functions. This approach combines a monotonicity analysis with a defined set of tests to demonstrate the accuracy of a software function over its entire input range. Unlike "standalone" dynamic methods, our approach provides full coverage, and guarantees a maximal error. We present a case study of the application of our approach to the analysis and testing of the software-implemented transfer function in a smart sensor. This demonstrated that relatively low levels of effort were needed to apply the approach. We conclude by discussing future developments of this approach.