Model-Based Test Cases Generation for Range-Sensitive Dataflow Coverage

Coverage criteria play a central role in software testing by providing objective measures of test suite adequacy and serving as a foundation for systematic test generation. Structural criteria – such as statement, branch, and dataflow coverage – enable verification of control and information dependencies within a program. At the same time, classical value-based techniques, including equivalence partitioning and boundary value analysis, are typically applied only to external inputs and do not account for the variability of values propagated within the program’s internal state. In many contemporary software systems, behavior is determined not only by control-flow structure or by the mere fact that variable uses are reached, but also by specific ranges of values propagated along execution paths. Traditional dataflow coverage criteria, in particular the all-uses criterion, consider a definition–use pair to be covered if it has been executed at least once, without distinguishing the values with which the variable reaches the use site. As a result, semantically significant yet narrow or domain-specific value ranges may remain untested, even when full structural coverage has been achieved. This limitation is especially critical for input-sensitive programs whose correctness depends on threshold conditions, numeric constraints, or implicit assumptions about admissible value ranges. Modern approaches to automated test generation, such as symbolic execution and model checking, partially account for value constraints; however, their coverage objectives typically remain structurally oriented. This creates a gap between dataflow analysis and systematic value-based testing, motivating the development of coverage criteria that are more sensitive to semantic distinctions. Objective. The goal of this work is to develop and formally justify a dataflow coverage criterion that accounts for semantically distinct value ranges of variables at use sites, and to design model-based methods for test case generation aimed at achieving such coverage. Results. We propose an extension of classical dataflow coverage by incorporating value-range distinctions at variable use points. Two complementary approaches to achieving this coverage are described: one based on symbolic modeling, and another based on model checking with Linear Temporal Logic specifications. Illustrative examples demonstrate that the proposed method reveals defects that remain undetected under traditional structural coverage criteria. Conclusions. The proposed approach integrates structural dataflow analysis with an explicit treatment of value variability, thereby providing semantically enriched test coverage. The criterion is intended to complement, rather than replace, existing approaches and appears particularly promising for testing input validation logic, detecting potential vulnerabilities, and also verifying cyber-physical systems. Although achieving such coverage may incur significant computational cost, it is justified for critical use points associated with external inputs and constraint checking.