Testing using CSP Models: Time, Inputs, and Outputs

James Baxter, Ana Cavalcanti, Maciej Gazda, Robert M. Hierons

Research output: Contribution to journalArticlepeer-review


The existing testing theories for CSP cater for verification of interaction patterns (traces) and deadlocks, but not time. We address here refinement and testing based on a dialect of CSP, called tock-CSP, which can capture discrete time properties. This version of CSP has been of widespread interest for decades; recently, it has been given a denotational semantics, and model checking has become possible using a well established tool. Here, we first equip tock-CSP with a novel semantics for testing, which distinguishes input and output events: the standard models of (tock-)CSP do not differentiate them, but for testing this is essential. We then present a new testing theory for timewise refinement, based on novel definitions of test and test execution. Finally, we reconcile refinement and testing by relating timed ioco testing and refinement in tock-CSP with inputs and outputs. With these results, this paper provides, for the first time, a systematic theory that allows both timed testing and timed refinement to be expressed. An important practical consequence is that this ensures that the notion of correctness used by developers guarantees that tests pass when applied to a correct system and, in addition, faults identified during testing correspond to development mistakes.

Original languageEnglish
Article number3572837
JournalACM Transactions on Computational Logic
Issue number2
Publication statusPublished - 28 Jan 2023

Bibliographical note

Funding Information:
Ana Cavalcanti and James Baxter are funded by the UK EPSRC (Engineering and Physical Sciences Research Council) under Grants No EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering under Grant No CiET1718/45. Maciej Gazda and Robert Mark Hierons are funded by the EPSRC, under Grant No EP/R025134/1.

Publisher Copyright:
© 2023 Association for Computing Machinery.


  • exhaustive test set
  • Model-based testing
  • process algebra
  • refinement

Cite this