Testing for Refinement in CSP

Abstract. CSP is a well-established formalism for modelling and verification of concurrent reactive systems based on refinement. Consolidated denotational models and an effective tool have encouraged much work on algebraic reasoning and model checking. Testing techniques based on CSP models, however, have not been widely explored, and in this paper we take a first step by instantiating a long standing theory of formal testing to CSP. We identify the testability hypothesis that we consider necessary to make the use of CSP feasible, define test sets that we prove to be exhaustive with respect to traces and failures refinement, and consider optimisations, inputs and outputs, and selection strategies. All our results are proved in terms of the CSP denotational models. They are a sound foundation for the development of test-generation techniques.

• Type: Conference
• Year: 2007
• Where: ICFEM
• Authors: Ana Cavalcanti, Marie-Claude Gaudel
• Keywords: Consolidated Denotational Models, CSP Denotational Models, Denotational Models, ICFEM 2007, Software Engineering