Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/13297
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Cavalcanti, A | - |
dc.contributor.author | Hierons, RM | - |
dc.contributor.author | Nogueira, S | - |
dc.contributor.author | Sampaio, A | - |
dc.date.accessioned | 2016-10-07T11:18:51Z | - |
dc.date.available | 2016-08-10 | - |
dc.date.available | 2016-10-07T11:18:51Z | - |
dc.date.issued | 2016 | - |
dc.identifier.citation | Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 3 - 13, (2016) | en_US |
dc.identifier.isbn | 9781509017638 | - |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/13297 | - |
dc.description.abstract | CSP is well established as a process algebra for refinement. Most refinement relations for CSP do not differentiate between inputs and outputs, and so are unsuitable for testing. This paper provides CSP with a denotational semantics based on suspension traces; it gives the traditional CSP operators a novel view, catering for the differences between inputs and outputs. We identify healthiness conditions for the suspension-Traces model and include a treatment of termination not contemplated in the context of input-output labelled transition systems. Using our suspension-Traces semantics, we provide for CSP a characterisation of the conformance relation ioco, which is widely used in testing. Finally, we propose a strategy to mechanise the verification of conformance according to ioco and suspension-Trace refinement using CSP tools. This work provides the basis for a theory of testing for CSP with inputs and outputs, and opens up the possibility of studying algebraic laws and compositional reasoning techniques based on ioco. Ultimately, it contributes to making CSP models useful for both design and testing of systems. | en_US |
dc.description.sponsorship | We thank Bill Roscoe for useful discussions. The work was carried out with the support of EPSRC hiJaC project, the CNPq (Brazil), INES, and the grants FACEPE 573964/2008-4, APQ-1037-1.03/08, CNPq 573964/2008-4, 476821/2011-8 and 249710/2013-7. | en_US |
dc.format.extent | 3 - 13 | - |
dc.language.iso | en | en_US |
dc.publisher | IEEE | en_US |
dc.title | A Suspension-Trace Semantics for CSP | en_US |
dc.type | Conference Paper | en_US |
dc.identifier.doi | http://dx.doi.org/10.1109/TASE.2016.9 | - |
dc.relation.isPartOf | Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 | - |
pubs.publication-status | Published | - |
Appears in Collections: | Dept of Computer Science Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 255.76 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.