caa a22 4500 445869720 CHVBK 20180317145508.0 cr unu---uuuuu 170323e20110401xx s 000 0 eng 10.1007/s00236-011-0133-z doi (NATIONALLICENCE)springer-10.1007/s00236-011-0133-z Testing for refinement in Circus [Elektronische Daten] [Ana Cavalcanti, Marie-Claude Gaudel] 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. Springer-Verlag, 2011 Cavalcanti Ana Department of Computer Science, University of York, YO10 5GH, York, England, UK aut Gaudel Marie-Claude Univ Paris-Sud, Laboratoire LRI, UMR8623, 91405, Orsay, France aut Acta Informatica Springer-Verlag 48/2(2011-04-01), 97-147 0001-5903 48:2<97 2011 48 236 https://doi.org/10.1007/s00236-011-0133-z text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s00236-011-0133-z text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Cavalcanti Ana Department of Computer Science, University of York, YO10 5GH, York, England, UK aut NATIONALLICENCE 700 1- Gaudel Marie-Claude Univ Paris-Sud, Laboratoire LRI, UMR8623, 91405, Orsay, France aut NATIONALLICENCE 773 0- Acta Informatica Springer-Verlag 48/2(2011-04-01), 97-147 0001-5903 48:2<97 2011 48 236 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer