Testing for refinement in Circus

TY - JOUR

T1 - Testing for refinement in Circus

AU - Cavalcanti, Ana

AU - Gaudel, Marie-Claude

PY - 2011/4/1

Y1 - 2011/4/1

N2 - 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.

AB - 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.

KW - unifying theories of programming

KW - formal testing

KW - symbolic testing

KW - process algebra

KW - CSP

KW - Z

UR - http://www.scopus.com/inward/record.url?scp=79952734993&partnerID=8YFLogxK

U2 - 10.1007/s00236-011-0133-z

DO - 10.1007/s00236-011-0133-z

M3 - Article

SN - 0001-5903

VL - 48

SP - 97

EP - 147

JO - Acta Informatica

JF - Acta Informatica

IS - 2

ER -