×

zbMATH — the first resource for mathematics

Test selection for traces refinement. (English) Zbl 1302.68086
Summary: Theories for model-based testing identify exhaustive test sets: typically infinite sets of tests whose execution establishes the conformance relation of interest. Practical techniques rely on selection strategies to identify finite subsets of these tests, and popular approaches are based on requirements to cover the model. In previous work, we have defined testing theories for refinement-based process algebra, namely, CSP and Circus, a state-rich process algebra. In this paper, we consider the selection of tests designed to establish traces refinement. In this case, conformance does not require that all traces of the model are available in the system under test, and this can raise challenges regarding coverage criteria for selection. To address these difficulties, we present a framework for formalising a variety of selection strategies. We exemplify its use in the formalisation of a selection criterion based on coverage of process communications for integration testing. We consider models written in Circus, whose symbolic testing theory facilitates the definition of uniformity and regularity hypotheses based on data operations, but also imposes extra challenges for selection of concrete tests. Our results, however, are relevant for any formalism where the conformance relation does not require all the traces of the specification to be executable by the system under test.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
Circus; CUTE; DART; PathCrawler; Pex; Z
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ball, T.; Burckhardt, S.; Coons, K. E.; Musuvathi, M.; Qadeer, S., Preemption sealing for efficient concurrency testing, (16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 6015, (2010), Springer), 420-434
[2] Barrett, G., Model checking in practice: the T9000 virtual channel processor, IEEE Trans. Softw. Eng., 21, 2, 69-78, (1995)
[3] Bentakouk, L.; Poizat, P.; Zaidi, F., Checking the behavioral conformance of web services with symbolic testing and an SMT solver, (Gogolla, M.; Wolff, B., Tests and Proofs, Lecture Notes in Computer Science, vol. 6706, (2011)), 33-50
[4] Bernot, G.; Gaudel, M.-C.; Marre, B., Software testing based on formal specifications: a theory and a tool, Softw. Eng. J., 6, 6, 387-405, (1991)
[5] Bron, A.; Farchi, E.; Magid, Y.; Nir, Y.; Ur, S., Applications of synchronization coverage, (ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, (2005)), 206-212
[6] Cadar, C.; Godefroid, P.; Khurshid, S.; Păsăreanu, C. S.; Sen, K.; Tillmann, N.; Visser, W., Symbolic execution for software testing in practice: preliminary assessment, (33rd International Conference on Software Engineering, (2011), ACM), 1066-1071
[7] Carver, R. H.; Tai, K.-C., Replay and testing for concurrent programs, IEEE Softw., 8, 2, 66-74, (1991)
[8] Carver, R. H.; Tai, Kuo-Chung, Use of sequencing constraints for specification-based testing of concurrent programs, IEEE Trans. Softw. Eng., 24, 471-490, (1998)
[9] Cavalcanti, A. L.C.; Clayton, P.; O’Halloran, C., From control law diagrams to ada via circus, Form. Asp. Comput., 23, 4, 465-512, (2011) · Zbl 1226.68028
[10] Cavalcanti, A. L.C.; Gaudel, M.-C., Testing for refinement in CSP, (9th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, vol. 4789, (2007), Springer-Verlag), 151-170
[11] Cavalcanti, A. L.C.; Gaudel, M.-C., A note on traces refinement and the \(c o n f\) relation in the unifying theories of programming, (Butterfield, A., Unifying Theories of Programming 2008, Lecture Notes in Computer Science, vol. 5713, (2010), Springer-Verlag)
[12] Cavalcanti, A. L.C.; Gaudel, M.-C., Specification coverage for testing in circus, (Qin, S., Unifying Theories of Programming, Lecture Notes in Computer Science, vol. 6445, (2010), Springer-Verlag), 1-45
[13] Cavalcanti, A. L.C.; Gaudel, M.-C., Testing for refinement in circus, Acta Inform., 48, 2, 97-147, (2011) · Zbl 1237.68059
[14] Cavalcanti, A. L.C.; Gaudel, M.-C., A note on test selection for conf refinement, (2013), Université de Paris-Sud, available at
[15] Cavalcanti, A. L.C.; Gaudel, M.-C., Data flow coverage for circus-based testing, (Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 8411, (2014)), 415-429
[16] Cavalcanti, A. L.C.; Hierons, R. M., Testing with inputs and outputs in CSP, (Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 7793, (2013)), 359-374
[17] Cavalcanti, A. L.C.; Sampaio, A. C.A.; Woodcock, J. C.P., A refinement strategy for circus, Form. Asp. Comput., 15, 2-3, 146-181, (2003)
[18] Dong, R. K.; Frankl, P. G., The ASTOOT approach to testing object-oriented programs, ACM Trans. Softw. Eng. Methodol., 3, 2, 103-130, (1994)
[19] Feliachi, A., Semantics-based testing for circus, (2012), LRI, Université de Paris-Sud, PhD thesis
[20] Feliachi, A.; Gaudel, M. C.; Wenzel, M.; Wolff, B., The circus testing theory revisited in isabelle/HOL, (Groves, L.; Sung, J., 15th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, vol. 8144, (2013), Springer), 243-260
[21] Fischer, C., How to combine Z with a process algebra, (Bowen, J.; Fett, A.; Hinchey, M., The Z Formal Specification Notation, (1998), Springer-Verlag)
[22] Frantzen, L.; Tretmans, J.; Willemse, T. A.C., A symbolic framework for model-based testing, (Havelund, K.; Núñez, M.; Rosu, G.; Wolff, B., Formal Approaches to Software Testing and Runtime Verification, Lecture Notes in Computer Science, vol. 4262, (2006), Springer), 40-54
[23] Freitas, L.; McDermott, J. P., Formal methods for security in the xenon hypervisor, Int. J. Softw. Tools Technol. Transf., 13, 5, 463-489, (2011)
[24] Fujiwara, S.; Bochmann, G., Testing non-deterministic finite state machines with fault coverage, (4th International Workshop on Protocol Test Systems, (1991), North-Holland Publishing Co.), 267-280
[25] Godefroid, P.; Klarlund, N.; Sen, K., DART: directed automated random testing, (ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, PLDI, (2005), ACM), 213-223
[26] Hall, A.; Chapman, R., Correctness by construction: developing a commercial secure system, IEEE Softw., 19, 1, 18-25, (2002)
[27] Hierons, R. M., Adaptive testing of a deterministic implementation against a nondeterministic finite state machine, Comput. J., 41, 5, 349-355, (1998) · Zbl 0921.68032
[28] Hierons, R. M., Comparing test sets and criteria in the presence of test hypotheses and fault domains, ACM Trans. Softw. Eng. Methodol., 11, 4, 427-448, (2002)
[29] Hierons, R. M., Applying adaptive test cases to nondeterministic implementations, Inform. Process. Lett., 98, 2, 56-60, (2006) · Zbl 1187.68162
[30] Hierons, R. M.; Ural, H., Reducing the cost of applying adaptive test cases, Computer Networks, 51, 1, 224-238, (2007) · Zbl 1118.68030
[31] Itoh, E.; Kawaguchi, Y.; Furukawa, Z.; Ushijima, K., Ordered sequence testing criteria for concurrent programs and the support tool, (1st Asia-Pacific Software Engineering Conference, (1994), IEEE), 236-245
[32] Larsen, K. G.; Mikucionis, M.; Nielsen, B.; Skou, A., Testing real-time embedded software using UPPAAL-TRON: an industrial case study, (5th ACM International Conference on Embedded Software, (2005), ACM), 299-306
[33] Lee, D.; Yannakakis, M., Principles and methods of testing finite state machines - a survey, (Proceedings of the IEEE, vol. 84, (1996)), 1090-1126
[34] Lei, Y.; Carver, R. H., Reachability testing of concurrent programs, IEEE Trans. Softw. Eng., 32, 6, 382-403, (2006)
[35] Lu, S.; Park, S.; Seo, E.; Zhou, Y., Learning from mistakes: a comprehensive study on real world concurrency bug characteristics, (International Conference on Architectural Support for Programming Languages and Operating Systems, (2008)), 329-339
[36] Mahony, B. P.; Dong, J. S., Blending object-Z and timed CSP: an introduction to TCOZ, (The 20th International Conference on Software Engineering (ICSE’98), (1998), IEEE Computer Society Press), 95-104
[37] Massink, M.; Latella, D.; Gnesi, S., On testing UML statecharts, J. Log. Algebr. Program., 69, 1-2, 1-74, (2006) · Zbl 1101.68014
[38] Miyazawa, A.; Cavalcanti, A. L.C., Refinement-oriented models of stateflow charts, Sci. Comput. Programming, 77, 10-11, 1151-1177, (2012) · Zbl 1243.68152
[39] Musuvathi, M.; Qadeer, S.; Ball, T.; Basler, G.; Arumuga Nainar, P.; Neamtiu, I., Finding and reproducing heisenbugs in concurrent programs, (Draves, R.; van Renesse, R., 8th USENIX Symposium on Operating Systems Design and Implementation, (2008), USENIX Association), 267-280
[40] De Nicola, R.; Hennessy, M. C.B., Testing equivalences for processes, Theoret. Comput. Sci., 3, 1-2, 83-133, (1984) · Zbl 0985.68518
[41] Nogueira, S.; Sampaio, A. C.A.; Mota, A. C., Guided test generation from CSP models, (Fitzgerald, J. S.; Haxthausen, A. E.; Yenigün, H., 5th International Colloquium on Theoretical Aspects of Computing, Lecture Notes in Computer Science, vol. 5160, (2008), Springer), 258-273 · Zbl 1161.68627
[42] Oliveira, M. V.M., Formal derivation of state-rich reactive programs using circus, (2006), University of York, PhD thesis
[43] Oliveira, M. V.M.; Cavalcanti, A. L.C.; Woodcock, J. C.P., A UTP semantics for circus, Form. Asp. Comput., 21, 1-2, 3-32, (2009) · Zbl 1165.68048
[44] Peleska, J.; Siegel, M., Test automation of safety-critical reactive systems, (Formal Methods Europe, Industrial Benefits and Advances in Formal Methods, Lecture Notes in Computer Science, vol. 1051, (1996))
[45] Peleska, J.; Siegel, M., Test automation of safety-critical reactive systems, S. Afr. Comput. J., 19, 53-77, (1997)
[46] Petrenko, A.; Yevtushenko, N.; Lebedev, A.; Das, A., Nondeterministic state machines in protocol conformance testing, (6th International Workshop on Protocol Test Systems VI, (1994), North-Holland Publishing Co.), 363-378
[47] Robinson-Mallett, C.; Hierons, R. M.; Liggesmeyer, P., Achieving communication coverage in testing, ACM SIGSOFT Softw. Eng. Notes, 31, 6, 1-10, (2006)
[48] Robinson-Mallett, C.; Hierons, R. M.; Poore, J.; Liggesmeyer, P., Using communication coverage criteria and partial model generation to assist software integration testing, Softw. Qual. Control, 16, 2, 185-211, (2008)
[49] Roggenbach, M., CSP-CASL: a new integration of process algebra and algebraic specification, Theoret. Comput. Sci., 354, 1, 42-71, (2006) · Zbl 1088.68132
[50] Roscoe, A. W., The theory and practice of concurrency, Prentice-Hall Series in Computer Science, (1998), Prentice-Hall
[51] Roscoe, A. W., Understanding concurrent systems, Texts in Computer Science, (2011), Springer · Zbl 1211.68205
[52] Schneider, S.; Treharne, H., Communicating B machines, (Bert, D.; Bowen, J.; Henson, M.; Robinson, K., ZB’2002: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, vol. 2272, (2002)), 416-435 · Zbl 1044.68121
[53] Sen, K.; Marinov, D.; Agha, G., CUTE: a concolic unit testing engine for C, (10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, (2005), ACM), 263-272
[54] Souza, S. R.S.; Souza, P. S.L.; Machado, M. C.C.; Camillo, M. S.; Simão, A. S.; Zaluska, E., Using coverage and reachability testing to improve concurrent program testing quality, (23rd International Conference on Software Engineering and Knowledge Engineering, (2011)), 207-212
[55] Taylor, R. N.; Levine, D. L.; Kelly, C. D., Structural testing of concurrent programs, IEEE Trans. Softw. Eng., 206-215, (1992)
[56] Tillmann, N.; de Halleux, J.; Schulte, W., Parameterized unit testing with pex: tutorial, (Borba, P. H.M.; Cavalcanti, A. L.C.; Sampaio, A. C.A.; Woodcock, J. C.P., Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, Lecture Notes in Computer Science, vol. 6153, (2010), Springer), 141-202
[57] Tretmans, J., Test generation with inputs, outputs, and quiescence, (Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 1055, (1996), Springer-Verlag), 127-146 · Zbl 0858.68061
[58] Tretmans, J.; Brinksma, E., Torx: automated model based testing, (1st European Conference on Model-Driven Software Engineering, (2003)), 13-25
[59] Veanes, M.; Campbell, C.; Schulte, W.; Kohli, P., On-the-fly testing of reactive systems, (2005), Microsoft Research, Technical report MSR-TR-2005-03
[60] Williams, N.; Marre, B.; Mouy, P.; Roger, M., Pathcrawler: automatic generation of path tests by combining static and dynamic analysis, (5th European Dependable Computing Conference, Lecture Notes in Computer Science, vol. 3463, (2005), Springer), 281-292
[61] Wong, W. E.; Lei, Y., Reachability graph-based test sequence generation for concurrent programs, Int. J. Softw. Eng. Knowl. Eng., 18, 6, 803-822, (2008)
[62] Woodcock, J. C.P.; Davies, J., Using Z—specification, refinement, and proof, (1996), Prentice-Hall · Zbl 0855.68060
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.