Data Flow Coverage for Circus-Based Testing

International audienceCircus is a state-rich process algebra based on Z and CSP that can be used for testing. In this paper, we consider data-flow coverage. In adapting the classical results on coverage of programs to Circus models, we define a notion of specification traces, consider models with data-flow anomalies, and cater for the internal nature of state. Our results are a framework for data-flow coverage of such abstract models, a novel data-flow criterion suited to state-rich process models, and the conversion of specification traces into symbolic traces