Using Formal Verification to Reduce Test Space of Fault-Tolerant Programs

Testing object-oriented programs is still a hard task, despite many studies on criteria to better cover the test space. Test criteria establish requirements one want to achieve in testing programs to help in finding software defects. On the other hand, program verification guarantees that a program...

Full description

Saved in:
Bibliographic Details
Main Authors: Xavier, K.S., Hanazumi, S., de Melo, A.C.V.
Format: Conference Proceeding
Language:English
Subjects:
Automatic testing
Computer science
Fault tolerance
Fault tolerant systems
Formal verification
Java
Mechanical factors
Programming
Software testing
System testing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Testing object-oriented programs is still a hard task, despite many studies on criteria to better cover the test space. Test criteria establish requirements one want to achieve in testing programs to help in finding software defects. On the other hand, program verification guarantees that a program preserves its specification but its application is not very straightforward in many cases. Both program testing and verification are expensive tasks and could be used to complement each other.This paper presents a new approach to automate and integrate testing and program verification for fault-tolerant systems. In this approach we show how to assess information from programs verification in order to reduce the test space regarding exceptions definition/use testing criteria. As properties on exception-handling mechanisms are checked using a model checker(Java PathFinder), programs are traced. Information from these traces can be used to realize how much testing criteria have been covered, reducing the further program test space.
ISSN:1551-0255
2160-7656
DOI:10.1109/SEFM.2008.31