Automated Test Generation for temporal specifications

Garima Bansal

Büchi automaton has been widely used in the speciﬁcation and formal veriﬁcation of linear temporal properties for reactive systems. Previously property-coverage testing has been developed to address the challenge of speciﬁcation-based testing with linear temporal properties. The core of property-coverage testing is a set of property-coverage metrics that formally measure test coverage on the syntactical and semantic structure of linear temporal properties. In this work we show that these metrics may also be used to derive test cases efﬁciently. We present Property Coverage Tester (PCT), an integrated and automated test case generation tool for speciﬁcation-based testing with linear temporal properties. PCT seamlessly integrates test generation algorithms, analysis tools, models, and their generated test cases, into one application. PCT implements model-checking-assisted test generation algorithms. These algorithms use counter-example generation capability of an off-the-shelf model checker to generate test cases. PCT provides capabilities to generate, analyze, and compare the effectiveness of test cases generated under different criteria. It helps developers choose appropriate criteria for their speciﬁc needs. We discuss in detail PCT's test generation algorithms and evaluation methodologies. PCT uses cross coverage and fault-injection-based sensitivity analysis to evaluate generated test cases. It helps a user select an appropriate test criterion for a given application. To evaluate PCT, we test it on applications selected from a variety of domains. Our test results show the effectiveness and efficiency of PCT and its underlying property-coverage testing techniques. We also present the Property/System Cyclomatic Complexity (PSCC), an empirical metric based on the cyclomatic complexity of models and property. PSCC estimates the quality of a property/system combination as a whole. We performed computational study on property/system pairs to evaluate the PSCC metric . Our results indicate a positive correlation between PSCC and the coverage of a requirement on a system model by the generated test suites. PCT and its underlying property-coverage testing techniques provide a holistic approach to debug a system and its linear temporal requirements, and a new way to extend the beneﬁts of linear temporal requirements to testing.

Automated Test Generation for temporal specifications

Files and links (1)

Abstract

Metrics

Details