Paper Info
Title
Testing for refinement in Circus
Abstract
Circus combines constructs to define complex data operations and interactions; it integrates Z and CSP, and, distinctively, it is a language for refinement that can describe programs as well as specification and design models. The semantics is based on the unifying theories of programming (UTP). Most importantly, Circus is representative of a class of refinement-oriented languages that combines facilities to specify abstract data types in a model-based style and patterns of interaction. What we present here is the Circus testing theory; this work is relevant as a foundation for sound test-generation techniques for a plethora of state-rich reactive languages. To cater for data operations, we define symbolic tests and exhaustive test sets. They are the basis for test-generation techniques that can combine coverage criteria for data and transition models. The notion of correctness is Circus refinement, a UTP-based generalisation of failures-divergences refinement that considers data modelling. Proof of exhaustivity exploits the correspondence between the operational and denotational semantics.
Year
DOI
Venue
2011
10.1007/s00236-011-0133-z
Acta Inf.
Keywords
DocType
Volume
test-generation technique,complex data operation,sound test-generation technique,denotational semantics,failures-divergences refinement,data operation,abstract data type,circus testing theory,circus refinement,utp-based generalisation
Journal
48
Issue
ISSN
Citations 
2
1432-0525
6
PageRank 
References 
Authors
0.49
18
2
Name
Order
Citations
PageRank
Ana Cavalcanti11407.68
Marie-Claude Gaudel269871.49