Journal
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC
Volume 21, Issue 3, Pages -Publisher
ASSOC COMPUTING MACHINERY
DOI: 10.1145/3379508
Keywords
Exhaustive test set; process algebra; refinement; refusal-testing model
Categories
Funding
- UK EPSRC (Engineering and Physical Sciences Research Council) [EP/M025756/1, EP/R025479/1]
- Royal Academy of Engineering [CiET1718/45]
- EPSRC [EP/R025134/1]
- CNPq (Brazilian National Research Council) [249710/2013-7]
- EPSRC [EP/M025756/1, EP/H017461/1, EP/R025479/1] Funding Source: UKRI
Ask authors/readers for more resources
This article addresses refinement and testing based on CSP models, when we distinguish input and output events. In a testing experiment, the tester (or the environment) controls the inputs, and the system under test controls the outputs. The standard models and refinement relations of CSP, however, do not differentiate inputs and outputs and are not, therefore, entirely suitable for testing. Here, we consider an alphabet of events partitioned into inputs and outputs, and we present a novel refusal-testing model for CSP with a notion of input-output refusal-traces refinement. We compare that with the ioco relation often used in testing, and we find that it is more widely applicable and stronger. This means that mistakes found using traditional ioco testing do indicate mistakes in the development. Finally, we provide a CSP testing theory that takes into account inputs and outputs. With our theory, it becomes feasible to develop techniques and tools for automatic generation of realistic and sound tests from CSP models. Our work reconciles the normally disparate areas of refinement and (formal) testing by identifying how ioco testing can be used to inform refinement-based results and vice-versa.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available