Specification Coverage for Testing in Circus

Abstract. The Unifying Theories of Programming underpins the development of Circus, a state-rich process algebra for refinement. We have previously presented a theory of testing for Circus; it gives a symbolic characterisation of tests. Each symbolic test specifies constraints that capture the effect of the possibly nondeterministic state operations, and their interaction. This is a sound basis for testing techniques based on constraint solving for generation of concrete tests, but does not support well selection criteria based on the structure of the specification. We present here a labelled transition system that captures information about a Circus model and its structure. It is useful for testing techniques based on specification coverage. The soundness argument for the new transition system follows the UTP style, but relates the new transition relation to the Circus relational model and its operational semantics.

• Type: Journal
• Year: 2010
• Where: UTP
• Authors: Ana Cavalcanti, Marie-Claude Gaudel
• Keywords: Circus, Circus Relational Model, Programming Languages, State-rich Process Algebra, UTP 2010