Date Added: Dec 2010
Dynamic specification mining observes program executions to infer models of normal program behavior. What makes one believe that the authors have seen sufficiently many executions? The TAUTOKO1 type state miner generates test cases that cover previously unobserved behavior, systematically extending the execution space and enriching the specification. To their knowledge, this is the first combination of systematic test case generation and type state mining - a combination with clear benefits: On a sample of 800 defects seeded into six Java subjects, a static type state verifier fed with enriched models would report significantly more true positives, and significantly fewer false positives than the initial models.