Dynamic Control Points and Independent Time Domains for Temporal Logic Falsification

摘要

Temporal logic falsification is an approach to model-based testing, where test cases are generated from a temporal logic specification and are run on a system-under-test to determine whether the system-under-test falsifies the temporal logic specification. In this paper, we report on two extensions on an existing temporal logic falsification approach, implemented in the S-Taliro tool. The two extensions concerns dynamically determining the number of control points in the process of search for test-cases and also, decoupling the different time domains in the n-dimensional input search space. We have conducted an experimental analysis of our approach on two benchmarks: an automatic transmission system (from the automotive domain) and a delta-sigma modulator (from the electrical domain). The results indicate a significant improvement over the existing approach. The full paper concerning this research is accepted for publication in the proceedings of A-MOST 2018.