2015 | OriginalPaper | Buchkapitel
Just Test What You Cannot Verify!
verfasst von : Mike Czech, Marie-Christine Jakobs, Heike Wehrheim
Erschienen in: Fundamental Approaches to Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Today, software verification is an established analysis method which can provide high guarantees for software safety. However, the resources (time and/or memory) for an exhaustive verification are not always available, and analysis then has to resort to other techniques, like testing. Most often, the already achieved
partial
verification results are discarded in this case, and testing has to start from scratch.
In this paper, we propose a method for combining verification and testing in which testing only needs to check the residual fraction of an uncompleted verification. To this end, the partial results of a verification run are used to construct a
residual program
(and residual assertions to be checked on it). The residual program can afterwards be fed into standard testing tools. The proposed technique is sound modulo the soundness of the testing procedure. Experimental results show that this combined usage of verification and testing can significantly reduce the effort for the subsequent testing.