Testing for refinement in CSP

Ana Cavalcanti; Marie-Claude Gaudel

Testing for refinement in CSP

Ana Cavalcanti, Marie-Claude Gaudel

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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, however, have not been widely explored, and in this paper we take a first step by instantiating Gaudel et al's theory of formal testing to CSP. We identify the testability hypothesis that we consider necessary to use CSP models as a basis for testing. We also 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. Our results are proved in terms of the CSP denotational models; they are a sound foundation for the development of test-generation techniques.

Original language	English
Title of host publication	FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS
Editors	M Butler, MG Hinchey, MM LarrondoPetrie
Place of Publication	BERLIN
Publisher	Springer
Pages	151-170
Number of pages	20
ISBN (Print)	978-3-540-76648-3
Publication status	Published - 2007
Event	9th International Conference on Formal Engineering Methods (ICFEM 2007) - Boca Raton Duration: 14 Nov 2007 → 15 Nov 2007

Conference

Conference	9th International Conference on Formal Engineering Methods (ICFEM 2007)
City	Boca Raton
Period	14/11/07 → 15/11/07

Keywords

ALGEBRAIC SPECIFICATIONS
GENERATION

ProCLaws: Programming from Control Laws
Cavalcanti, A. L. C.
EPSRC
1/07/07 → 30/09/11
Project: Research project (funded) › Research

Cite this

@inproceedings{1f6676496ca24529aa0e73b89098347e,

title = "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, however, have not been widely explored, and in this paper we take a first step by instantiating Gaudel et al's theory of formal testing to CSP. We identify the testability hypothesis that we consider necessary to use CSP models as a basis for testing. We also 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. Our results are proved in terms of the CSP denotational models; they are a sound foundation for the development of test-generation techniques.",

keywords = "ALGEBRAIC SPECIFICATIONS, GENERATION",

author = "Ana Cavalcanti and Marie-Claude Gaudel",

year = "2007",

language = "English",

isbn = "978-3-540-76648-3",

pages = "151--170",

editor = "M Butler and MG Hinchey and MM LarrondoPetrie",

booktitle = "FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS",

publisher = "Springer",

address = "Germany",

note = "9th International Conference on Formal Engineering Methods (ICFEM 2007) ; Conference date: 14-11-2007 Through 15-11-2007",

}

TY - GEN

T1 - Testing for refinement in CSP

AU - Cavalcanti, Ana

AU - Gaudel, Marie-Claude

PY - 2007

Y1 - 2007

N2 - 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, however, have not been widely explored, and in this paper we take a first step by instantiating Gaudel et al's theory of formal testing to CSP. We identify the testability hypothesis that we consider necessary to use CSP models as a basis for testing. We also 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. Our results are proved in terms of the CSP denotational models; they are a sound foundation for the development of test-generation techniques.

AB - 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, however, have not been widely explored, and in this paper we take a first step by instantiating Gaudel et al's theory of formal testing to CSP. We identify the testability hypothesis that we consider necessary to use CSP models as a basis for testing. We also 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. Our results are proved in terms of the CSP denotational models; they are a sound foundation for the development of test-generation techniques.

KW - ALGEBRAIC SPECIFICATIONS

KW - GENERATION

M3 - Conference contribution

SN - 978-3-540-76648-3

SP - 151

EP - 170

BT - FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS

A2 - Butler, M

A2 - Hinchey, MG

A2 - LarrondoPetrie, MM

PB - Springer

CY - BERLIN

T2 - 9th International Conference on Formal Engineering Methods (ICFEM 2007)

Y2 - 14 November 2007 through 15 November 2007

ER -

Testing for refinement in CSP

Abstract

Conference

Keywords

Projects

ProCLaws: Programming from Control Laws

Cite this