By the same authors

From the same journal

Testing for refinement in Circus

Research output: Contribution to journalArticle



Publication details

JournalActa Informatica
DatePublished - 1 Apr 2011
Issue number2
Number of pages51
Pages (from-to)97-147
Original languageEnglish


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.

    Research areas

  • unifying theories of programming, formal testing, symbolic testing, process algebra, CSP, Z


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations