Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java PathfinderWe present work on a prototype tool based on the JavaPathfinder (JPF) model checker for automatically generating tests satisfying the MC/DC code coverage criterion. Using the Eclipse IDE, developers and testers can quickly instrument Java source code with JPF annotations covering all MC/DC coverage obligations, and JPF can then be used to automatically generate tests that satisfy these obligations. The prototype extension to JPF enables various tasks useful in automatic test generation to be performed, such as test suite reduction and execution of generated tests.
Document ID
20100024475
Acquisition Source
Ames Research Center
Document Type
Conference Paper
Authors
Staats, Matt (Minnesota Univ. MN, United States)
Date Acquired
August 24, 2013
Publication Date
April 1, 2009
Publication Information
Publication: Proceedings of the First NASA Formal Methods Symposium