Symbolic Path-guided Test Cases for Models with Data and Time

TL;DR

This paper presents a method for generating test cases from timed symbolic transition systems using symbolic execution on data and time, producing finite symbolic trees aligned with user-defined test purposes.

Contribution

It introduces a novel approach combining symbolic execution with timed transition systems to generate test cases that consider data and timing constraints.

Findings

Test cases effectively handle data and time constraints.

Generated test cases are finite symbolic trees with verdicts.

Method improves test coverage for timed systems.

Abstract

This paper focuses on generating test cases from timed symbolic transition systems. At the heart of the generation process are symbolic execution techniques on data and time. Test cases look like finite symbolic trees with verdicts on their leaves and are based on a user-specified finite symbolic path playing the role of a test purpose. Generated test cases handle data involved in time constraints and uninitialized parameters, leveraging the advantages of symbolic execution techniques.