More Web Proxy on the site http://driver.im/

research-article

Inputs and Outputs in CSP: A Model and a Testing Theory

Authors:

Ana Cavalcanti,

Robert M. Hierons,

Sidney NogueiraAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 21, Issue 3

Article No.: 24, Pages 1 - 53

https://doi.org/10.1145/3379508

Published: 18 May 2020 Publication History

Abstract

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.

References

[1]

G. Barrett. 1995. Model checking in practice: The T9000 virtual channel processor. IEEE Trans. Softw. Eng. 21, 2 (1995), 69--78.

Digital Library

[2]

M. Bijl, A. Rensink, and J. Tretmans. 2003. Component-based Testing with ioco. Technical Report. University of Twente. CTIT Technical Report TR CTIT 03 34.

[3]

I. B. Bourdonov, A. Kossatchev, and V. V. Kuliamin. 2006. Formal conformance testing of systems with refused inputs and forbidden actions. Electr. Notes Theoret. Comput. Sci. 164, 4 (2006), 83--96.

[4]

E. Brinksma. 1988. A theory for the derivation of tests. In Protocol Specification, Testing, and Verification VIII. North-Holland, 63--74.

[5]

E. Brinksma, L. Heerink, and J. Tretmans. 1998. Factorized test generation for multi-input/output transition systems. In Proceedings of the 11th IFIP Workshop on Testing of Communicating Systems. Kluwer Academic Publishers, 67--82.

[6]

L. B. Briones and E. Brinksma. 2005. Testing real-time multi input-output systems. In Proceedings of the 7th International Conference on Formal Engineering Methods (Lecture Notes in Computer Science), Vol. 3785. Springer, 264--279.

[7]

A. L. C. Cavalcanti and M.-C. Gaudel. 2007. Testing for refinement in CSP. In Proceedings of the 9th International Conference on Formal Engineering Methods (Lecture Notes in Computer Science), Vol. 4789. Springer-Verlag, 151--170.

[8]

A. L. C. Cavalcanti and M.-C. Gaudel. 2014. Data flow coverage for Circus-based testing. In Proceedings of the Conference on Fundamental Approaches to Software Engineering (Lecture Notes in Computer Science), Vol. 8441. 415--429.

Digital Library

[9]

A. L. C. Cavalcanti, M.-C. Gaudel, and R. M. Hierons. 2011. Conformance relations for distributed testing based on CSP. In Proceedings of the IFIP International Conference on Testing Software and Systems (Lecture Notes in Computer Science), B. Wolff and F. Zaidi (Eds.). Springer-Verlag.

[10]

A. L. C. Cavalcanti, R. Hierons, and S. Nogueira. 2017. Input and Outputs in CSP: A Model and a Testing Theory. Technical Report. University of York, Department of Computer Science, York, UK. Retrieved from www-users.cs.york.ac.uk/&sim;alcc/CHN17.pdf.

[11]

A. L. C. Cavalcanti and R. M. Hierons. 2012. Testing with Inputs and Outputs in CSP—Extended Version. Technical Report. Retrieved from www-users.cs.york.ac.uk/&sim;alcc/CH12.pdf.

[12]

A. L. C. Cavalcanti and R. M. Hierons. 2013. Testing with inputs and outputs in CSP. In Fundamental Approaches to Software Engineering (Lecture Notes in Computer Science), Vol. 7793. 359--374.

[13]

A. L. C. Cavalcanti, R. M. Hierons, S. Nogueira, and A. C. A. Sampaio. 2016. A suspension-trace semantics for CSP. In Proceedings of the International Symposium on Theoretical Aspects of Software Engineering. 3--13. Invited paper.

[14]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. 2003. A refinement strategy for circus. Formal Aspects Comput. 15, 2--3 (2003), 146--181.

[15]

A. Feliachi, M. C. Gaudel, M. Wenzel, and B. Wolff. 2013. The circus testing theory revisited in Isabelle/HOL. In Proceedings of the 15th International Conference on Formal Engineering Methods (Lecture Notes in Computer Science), L. Groves and J. Sung (Eds.), Vol. 8144. Springer, 243--260.

[16]

C. Fischer. 1998. How to combine Z with a process algebra. In The Z Formal Specification Notation, J. Bowen, A. Fett, and M. Hinchey (Eds.). Springer-Verlag.

[17]

T. Gibson-Robinson, P. Armstrong, A. Boulgakov, and A. W. Roscoe. 2014. FDR3—A modern refinement checker for CSP. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. 187--201.

[18]

C. Gregorio-Rodríguez, L. Llana, and R. Martínez. 2018. An axiomatic semantics for iocos conformance relation. J. Logic. Alg. Methods Program. 100 (2018), 152--184.

[19]

C. Gregorio-Rodríguez, L. Llana, and R. Martínez-Torres. 2013. Input-output conformance simulation (iocos) for model-based testing. In Formal Techniques for Distributed Systems, D. Beyer and M. Boreale (Eds.). Springer, 114--129.

[20]

A. Hall and R. Chapman. 2002. Correctness by construction: Developing a commercial secure system. IEEE Softw. 19, 1 (2002), 18--25.

Digital Library

[21]

L. Heerink and J. Tretmans. 1997. Refusal testing for classes of transition systems with inputs and outputs. In Proceedings of the Conference on Formal Description Techniques and Protocol Specification, Testing, and Verification (IFIP’97), Vol. 107. Chapman 8 Hall, 23--38.

[22]

C. A. R. Hoare and He Jifeng. 1998. Unifying Theories of Programming. Prentice-Hall.

[23]

M. B. Josephs. 1992. Receptive process theory. Acta Informat. 29, 1 (1992), 17--31.

Digital Library

[24]

T. Kahsai, M. Roggenbach, and B.-H. Schlingloff. 2007. Specification-based testing for refinement. In Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods. IEEE Computer Society, 237--246.

[25]

M. Krichen. 2010. A formal framework for conformance testing of distributed real-time systems. In Proceedings of the Conference on Principles of Distributed Systems, C. Lu, T. Masuzawa, and M. Mosbah (Eds.). Lecture Notes in Computer Science, Vol. 6490. Springer, 139--142.

[26]

G. Lowe. 2008. Specification of communicating processes: Temporal logic versus refusals-based refinement. Formal Aspects Comput. 20, 3 (2008), 277--294.

[27]

B. P. Mahony and J. S. Dong. 1998. Blending object-Z and timed CSP: An introduction to TCOZ. In Proceedings of the 20th International Conference on Software Engineering (ICSE’98). IEEE Computer Society Press, 95--104.

[28]

R. Milner. 1989. Communication and Concurrency. Prentice-Hall.

Digital Library

[29]

A. Mukarram. 1993. A Refusal Testing Model for CSP. Ph.D. Dissertation. Department of Computer Science, University of Oxford.

[30]

S. Nogueira, A. C. A. Sampaio, and A. C. Mota. 2014. Test generation from state-based use case models. Formal Aspects Comput. 26, 3 (2014), 441--490.

[31]

I. Phillips. 1987. Refusal testing. Theoret. Comput. Sci. 50, 3 (1987), 241--284.

Digital Library

[32]

M. Roggenbach. 2006. CSP-CASL: A new integration of process algebra and algebraic specification. Theoret. Comput. Sci. 354, 1 (2006), 42--71.

Digital Library

[33]

A. W. Roscoe. 1998. The Theory and Practice of Concurrency. Prentice-Hall.

Digital Library

[34]

A. W. Roscoe. 2011. Understanding Concurrent Systems. Springer.

Digital Library

[35]

A. C. A. Sampaio, S. Nogueira, A. Mota, and Y. Isobe. 2014. Sound and mechanised compositional verification of input-output conformance. Softw. Test. Verificat. Reliabil. 24, 4 (2014), 289--319.

Digital Library

[36]

S. Schneider and H. Treharne. 2002. Communicating B machines. In Proceedings of the Conference on Formal Specification and Development in Z and B(ZB’02) (Lecture Notes in Computer Science), D. Bert, J. Bowen, M. Henson, and K. Robinson (Eds.), Vol. 2272. 416--435.

[37]

J. Tretmans. 1992. A Formal Approach to Conformance Testing. Ph.D. Dissertation. University of Twente, Enschede, The Netherlands.

[38]

J. Tretmans. 1996. Test generation with inputs, outputs, and quiescence. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), Vol. 1055. Springer-Verlag, 127--146.

[39]

J. Tretmans. 1996. Test generation with inputs, outputs and repetitive quiescence. Softw. Concepts Tools 17, 3 (1996), 103--120.

[40]

J. Tretmans. 2008. Model-based testing with labelled transition systems, in Formal Methods and Testing. Springer-Verlag, 1--38.

[41]

J. Tretmans and E. Brinksma. 2003. TorX: Automated model-based testing. In Proceedings of the 1st European Conference on Model-Driven Software Engineering. 13--25.

[42]

M. van der Bijl, A. Rensink, and J. Tretmans. 2004. Compositional testing with ioco. In Proceedings of the Conference on Formal Approaches to Software Testing, A. Petrenko and A. Ulrich Andreas (Eds.). Lecture Notes in Computer Science, Vol. 2931. Springer, 86--100.

[43]

M. Weiglhofer and B. Aichernig. 2010. Unifying input output conformance. In Proceedings of the Conference on Unifying Theories of Programming, A. Butterfield (Ed.). Lecture Notes in Computer Science, Vol. 5713. Springer, 181--201.

[44]

T. A. C. Willemse. 2006. Heuristics for ioco-based test-based modelling. In Proceedings of the Conference on Formal Methods: Applications and Technology (Lecture Notes in Computer Science), L. Brim, B. Haverkort, M. Leucker, and J. van de Pol (Eds.), Vol. 4346. Springer, 132--147.

[45]

J. C. P. Woodcock and J. Davies. 1996. Using Z-Specification, Refinement, and Proof. Prentice-Hall.

Cited By

Gazda MHierons R(2025)Model independent refusal trace testingScience of Computer Programming10.1016/j.scico.2024.103173239:COnline publication date: 1-Jan-2025
https://dl.acm.org/doi/10.1016/j.scico.2024.103173
Baxter JCavalcanti AGazda MHierons R(2023)Testing using CSP Models: Time, Inputs, and OutputsACM Transactions on Computational Logic10.1145/357283724:2(1-40)Online publication date: 28-Jan-2023
https://dl.acm.org/doi/10.1145/3572837
Núñez MHierons RLefticaru R(2023)Implementation relations and testing for cyclic systems: Adding probabilitiesRobotics and Autonomous Systems10.1016/j.robot.2023.104426165(104426)Online publication date: Jul-2023
https://doi.org/10.1016/j.robot.2023.104426
Show More Cited By

Index Terms

Inputs and Outputs in CSP: A Model and a Testing Theory
1. Computing methodologies
  1. Concurrent computing methodologies
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Testing using CSP Models: Time, Inputs, and Outputs
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 ...
Testing with inputs and outputs in CSP
FASE'13: Proceedings of the 16th international conference on Fundamental Approaches to Software Engineering

This paper addresses refinement and testing based on CSP models, when we distinguish input and output events. From a testing perspective, there is an asymmetry: the tester (or the environment) controls the inputs, and the system under test controls the ...
Fault-based refinement-testing for CSP

The process algebra CSP has been studied as a notation for model-based testing. Theoretical and practical work has been developed using its trace and failure semantics, and their refinement notions as conformance relations. Two sets of tests have been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 21, Issue 3

July 2020

407 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3384674

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 May 2020

Online AM: 07 May 2020

Accepted: 01 January 2020

Revised: 01 December 2019

Received: 01 February 2018

Published in TOCL Volume 21, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
132
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gazda MHierons R(2025)Model independent refusal trace testingScience of Computer Programming10.1016/j.scico.2024.103173239:COnline publication date: 1-Jan-2025
https://dl.acm.org/doi/10.1016/j.scico.2024.103173
Baxter JCavalcanti AGazda MHierons R(2023)Testing using CSP Models: Time, Inputs, and OutputsACM Transactions on Computational Logic10.1145/357283724:2(1-40)Online publication date: 28-Jan-2023
https://dl.acm.org/doi/10.1145/3572837
Núñez MHierons RLefticaru R(2023)Implementation relations and testing for cyclic systems: Adding probabilitiesRobotics and Autonomous Systems10.1016/j.robot.2023.104426165(104426)Online publication date: Jul-2023
https://doi.org/10.1016/j.robot.2023.104426
Gazda MHierons R(2023)Removing redundant refusals: Minimal complete test suites for failure trace semanticsInformation and Computation10.1016/j.ic.2023.105009291(105009)Online publication date: Mar-2023
https://doi.org/10.1016/j.ic.2023.105009
Gazda MHierons RGorla D(2021)Removing redundant refusalsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470737(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470737
Yalan YWei T(2021)Deep Logistic Learning Framework for E-Commerce and Supply Chain Management PlatformArabian Journal for Science and Engineering10.1007/s13369-021-05894-zOnline publication date: 2-Aug-2021
https://doi.org/10.1007/s13369-021-05894-z

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents