My research on software testing emphasizes on specification-based testing with temporal logic requirements. Verification and Validation (V&V) activities generally account for 50-70% of the cost of developing safety-critical software, and a large amount of that cost is spent on testing. Meanwhile, due to recent advances in formal verification, formal techniques such as model checking is gaining great momentum in research and industrial practices. Model checking verifies a system model against its formal requirement in temporal logics. Efficient model checking algorithms and tools have been developed for verifying large-scale system designs. Specification-based testing with temporal logic requirements capitalizes on these opportunities to improve the efficiency and effectiveness of testing. To improve test effectiveness, specification-based testing with temporal logic requirements centers the testing around formal requirements using temporal-logic-based test metrics and criteria. To improve test efficiency, we developed model-checking-assisted test generation algorithms extend off-the-shelf model checkers to generate test cases for property coverage criterion.

We developed a property-coverage testing framework with Linear Temporal Logic (LTL), one of the first works in specification-based testing covering temporal logic properties.  Since then, we have been focusing semantics-orient approaches to cover actual semantics, not just syntax, of temporal properties. We defined several coverage metrics and criteria  for formal requirements in Buchi automaton, and developed efficient model-checking-assisted test generation algorithms for these new criteria. We also developed an unified framework and a tool to compare the performance of various test criteria used with model-checking-assisted test case generation. 

Figure 1. Workflow of specification testing with Buchi Automata[TZ14a]

Figure 2. Work flow of property refinement enabled by property coverage metrics [TZ14a]

Publications

1. Bolong Zeng and Li Tan: "Testing with Buchi Automata: Transition coverage metrics, performance analysis, and property refinement". In Press. Advances in Intelligent Systems and Computing. Springer. 2015
2. Li Tan and Bolong Zeng: "Specification-Based Testing with Buchi Automata: Transition Coverage Criteria and Property Refinement". Proceedings of 2014 IEEE Information Reuse and Integration (IEEE IRI'14). IEEE Press. San Francisco, CA. August, 2014.
3. Bolong Zeng and Li Tan: "A Unified Framework for Evaluating Test Criteria. in Model-Checking-Assisted Test Case Generation". Information Systems Frontiers. Springer. April, 2013.
4. Bolong Zeng and Li Tan: "Test Criteria for Model-Checking-Assisted Test Vector Generation: A Computational Study". In the Proceedings of 2012 IEEE Information Reuse and Integration (IEEE IRI'12). IEEE Press. Las Vegas, NV. August, 2012.
5. Li Tan: "State Coverage Metrics for Specification-Based Testing with Buchi Automata". In Proceedings of the 5th International Conference on Tests and Proofs. Zurich, Switzerland. In the Lecture Notes in Computer Science. Springer-Verlag. June 30-July 01, 2011.
6. Linmin Yang, Zhe Dang, Thomas R. Fischer, Min Sik Kim and Li Tan: "Entropy and Software Systems: Towards an Information-Theoretic Foundation of Software Testing". In Proceedings of the ACM Sigsoft FSE/SDP workshop on Future of software engineering research (FSE-FoSER'10). ACM press. Santa Fe, New Mexico. November, 2010.
7. Li Tan, Oleg Sokolsky, and Insup Lee. " Specification-based Testing with Linear Temporal Logic", In the proceedings of IEEE Internation Conference on Information Reuse and Integration (IRI'04), IEEE society, 2004.
8. Li Tan, Oleg Sokolsky, and Insup Lee. "Property-Coverage Testing". Technical report MS-CIS-03-02. Department of Computer and Information Science, University of Pennsylvania. January, 2003.