Testing using CSP Models: Time, Inputs, and Outputs

TY - JOUR

T1 - Testing using CSP Models

T2 - Time, Inputs, and Outputs

AU - Baxter, James

AU - Cavalcanti, Ana

AU - Gazda, Maciej

AU - Hierons, Robert M.

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

PY - 2023/1/28

Y1 - 2023/1/28

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

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

KW - exhaustive test set

KW - Model-based testing

KW - process algebra

KW - refinement

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

U2 - 10.1145/3572837

DO - 10.1145/3572837

M3 - Article

AN - SCOPUS:85152491032

SN - 1529-3785

VL - 24

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 2

M1 - 3572837

ER -