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

Bishop, P. G., Bloomfield, R. E. & Cyra, L. (2013). Combining Testing and Proof to Gain High Assurance in Software: a Case Study. Paper presented at the IEEE International Symposium on Software Reliability Engineering (ISSRE 2013), 4 - 7 Nov 2013, Pasadena, CA, USA.

[img]
Preview
PDF
Download (263kB) | Preview
Official URL: http://2013.issre.net/

Abstract

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.

Item Type: Conference or Workshop Item (Paper)
Uncontrolled Keywords: test strategies, static analysis, formal proof
Subjects: Q Science > QA Mathematics > QA76 Computer software
Divisions: School of Informatics > Centre for Software Reliability
URI: http://openaccess.city.ac.uk/id/eprint/2608

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics