Test-Case Generation with Automata-Based Software Model Checking
摘要
Software quality is often evaluated by testing the software on an adequate test suite, e.g., a test suite achieving certain or high coverage of the software. Manually generating such test suites is tedious. Thus, several automatic test-case generation approaches were developed to support this task. Approaches based on software model checking typically achieve high coverage and have been shown to be sufficiently efficient in the past. Yet, there does not exist a test-case generation approach that builds upon the automata-based approach to software model checking e.g., successfully used by Ultimate Automizer. To close this methodical gap, we present Ultimate TestGen, a test-case generator built on Ultimate Automizer. An experimental comparison of Ultimate TestGen against a closely related, up-to-date test-case generation approach reveals that Ultimate TestGen generates test suites that achieve the same or higher branch coverage for nearly 75% of the evaluated programs.