Subscribe

Issue No.09 - Sept. (2013 vol.39)

pp: 1216-1229

Wilkerson L. Andrade , Federal University of Campina Grande, Campina Grande

Patricia D.L. Machado , Federal University of Campina Grande, Campina Grande

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2013.13

ABSTRACT

The state space explosion problem is one of the challenges to be faced by test case generation techniques, particularly when data values need to be enumerated. This problem gets even worse for real-time systems (RTS) that also have time constraints. The usual solution in this context, based on finite state machines or time automata, consists of enumerating data values (restricted to finite domains) while treating time symbolically. In this paper, a symbolic model for conformance testing of real-time systems software named TIOSTS that addresses both data and time symbolically is presented. Moreover, a test case generation process is defined to select more general test cases with variables and parameters that can be instantiated at testing execution time. Generation is based on a combination of symbolic execution and constraint solving for the data part and symbolic analysis for timed aspects. Furthermore, the practical application of the process is investigated through a case study.

INDEX TERMS

Testing, Clocks, Cost accounting, Real-time systems, Data models, Automata, Semantics, testing strategies, Real-time systems and embedded systems, formal methods, symbolic execution

CITATION

Wilkerson L. Andrade, Patricia D.L. Machado, "Generating Test Cases for Real-Time Systems Based on Symbolic Models",

*IEEE Transactions on Software Engineering*, vol.39, no. 9, pp. 1216-1229, Sept. 2013, doi:10.1109/TSE.2013.13REFERENCES

- [1] J. Tretmans, "Testing Concurrent Systems: A Formal Approach,"
Proc. 10th Int'l Conf. Concurrency Theory, pp. 46-65, 1999.- [2] A. Hessel, K.G. Larsen, B. Nielsen, P. Pettersson, and A. Skou, "Time-Optimal Real-Time Test Case Generation Using UPPAAL,"
Proc. Third Int'l Workshop Formal Approaches to Testing of Software, pp. 114-130, 2004.- [3] K. Larsen, M. Mikucionis, and B. Nielsen, "Online Testing of Real-Time Systems Using UPPAAL,"
Proc. Int'l Workshop Formal Approaches to Testing of Software, pp. 79-94, 2005.- [4] M. Krichen and S. Tripakis, "Conformance Testing for Real-Time Systems,"
Formal Methods in Systems Design, vol. 34, no. 3, pp. 238-304, 2009.- [5] N. Bertrand, T. Jéron, A. Stainer, and M. Krichen, "Off-Line Test Selection with Test Purposes for Non-Deterministic Timed Automata,"
Proc. 17th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 96-111, 2011.- [6] S. Li, J. Wang, W. Dong, and Z.-C. Qi, "Property-Oriented Testing of Real-Time Systems,"
Proc. 11th Asia-Pacific Software Eng. Conf., pp. 358-365, 2004.- [7] A. En-Nouaary, R. Dssouli, and F. Khendek, "Timed WP-Method: Testing Real-Time Systems,"
IEEE Trans. Software Eng., vol. 28, no. 11, pp. 1023-1038, Nov. 2002.- [8] M. Merayo, M. Núñez, and I. Rodríguez, "Extending EFSMs to Specify and Test Timed Systems with Action Durations and Time-Outs,"
IEEE Trans. Computers, vol. 57, no. 6, pp. 835-844, June 2008.- [9] L. Frantzen, J. Tretmans, and T. Willemse, "A Symbolic Framework for Model-Based Testing,"
Proc. First Combined Int'l Conf. Formal Approaches to Software Testing and Runtime Verification, pp. 40-54, 2006.- [10] B. Jeannet, T. Jéron, V. Rusu, and E. Zinovieva, "Symbolic Test Selection Based on Approximate Analysis,"
Proc. 11th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 349-364, 2005.- [11] G. Lestiennes and M.-C. Gaudel, "Testing Processes from Formal Specifications with Inputs, Outputs and Data Types,"
Proc. 13th Int'l Symp. Software Reliability Eng., pp. 3-14, 2002.- [12] V. Rusu, L. du Bousquet, and T. Jéron, "An Approach to Symbolic Test Generation,"
Proc. Second Int'l Conf. Integrated Formal Methods, pp. 338-357, 2000.- [13] S. von Styp, H. Bohnenkamp, and J. Schmaltz, "A Conformance Testing Relation for Symbolic Timed Automata,"
Proc. Eighth Int'l Conf. Formal Modeling and Analysis of Timed Systems, pp. 243-255, 2010.- [14] O.N. Timo, H. Marchand, and A. Rollet, "Automatic Test Generation for Data-Flow Reactive Systems with Time Constraints,"
Proc. Fourth IEEE Int'l Conf. Software Testing, Verification and Validation Workshops, pp. 25-30, 2010.- [15] O.N. Timo and A. Rollet, "Conformance Testing of Variable Driven Automata,"
Proc. Eighth IEEE Int'l Workshop Factory Comm. Systems, pp. 241-248, 2010.- [16] O.N. Timo and A. Rollet, "Test Selection for Data-Flow Reactive Systems Based on Observations,"
Proc. Fourth IEEE Int'l Conf. Software Testing, Verification and Validation Workshops, pp. 1-8, Mar. 2011.- [17] W.L. Andrade, P.D.L. Machado, T. Jéron, and H. Marchand, "Abstracting Time and Data for Conformance Testing of Real-Time Systems,"
Proc. Fourth IEEE Int'l Conf. Software Testing, Verification and Validation Workshops, pp. 9-17, Mar. 2011.- [18] R. Cardell-Oliver, "Conformance Tests for Real-Time Systems with Timed Automata Specifications,"
Formal Aspects of Computing, vol. 12, no. 5, pp. 350-371, Dec. 2000.- [19] K.G. Larsen, P. Pettersson, and W. Yi, "UPPAAL in a Nutshell,"
Int'l J. Software Tools of Technology Transfer, vol. 1, no. 1, pp. 134-152, 1997.- [20] W.L. Andrade, P.D.L. Machado, E.L.G. Alves, and D.R. Almeida, "Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS,"
Proc. 12th Brazilian Symp. Formal Methods: Foundations and Applications, pp. 54-69, 2009.- [21] A.Q. Macedo, W.L. Andrade, D.R. Almeida, and P.D.L. Machado, "Automating Test Case Execution for Real-Time Embedded Systems,"
Proc. Fourth IEEE Int'l Conf. Software Testing, Verification and Validation Workshops, pp. 37-42, 2010.- [22] The FreeRTOS.org Project, http:/www.freertos.org, 2013.
- [23] W.L. Andrade, "Symbolic Model-Based Testing for Real-Time Systems," PhD dissertation, Fed. Univ. of Campina Grande, http://splab.computacao.ufcg.edu.br/doctoral-theses splab- thesis-2011-04-andrade , Apr. 2011.
- [24] R. Ehlers, D. Fass, M. Gerke, and H.-J. Peter, "Fully Symbolic Timed Model Checking Using Constraint Matrix Diagrams,"
Proc. 31st IEEE Real-Time Systems Symp., pp. 360-371, 2010.- [25] S. Seshia and R. Bryant, "Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods,"
Proc. 15th Int'l Conf. Computer Aided Verification, pp. 154-166, 2003.- [26] R. Alur and D.L. Dill, "A Theory of Timed Automata,"
Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.- [27] S. Bornot, J. Sifakis, and S. Tripakis, "Modeling Urgency in Timed Systems,"
Proc. Int'l Conf. Compositionality: The Significant Difference, pp. 264-279, 1998.- [28] T. Jéron, H. Marchand, and V. Rusu, "Symbolic Determinisation of Extended Automata,"
Proc. Fourth IFIP Int'l Conf. Theoretical Computer Science. pp. 197-212, 2006.- [29] L.A. Clarke, "A System to Generate Test Data and Symbolically Execute Programs,"
IEEE Trans. Software Eng., vol. 2, no. 3, pp. 215-222, Sept. 1976.- [30] J.C. King, "A New Approach to Program Testing,"
Proc. Int'l Conf. Reliable Software, pp. 228-233, 1975.- [31] C. Gaston, P. Le Gall, N. Rapin, and A. Touil, "Symbolic Execution Techniques for Test Purpose Definition,"
Proc. 18th IFIP TC6/WG6.1 Int'l Conf. Testing of Communicating Systems, pp. 1-18, 2006.- [32] E. Jöbstl, M. Weiglhofer, B.K. Aichernig, and F. Wotawa, "When BDDs Fail: Conformance Testing with Symbolic Execution and SMT Solving,"
Proc. Third Int'l Conf. Software Testing, Verification and Validation, pp. 479-488, 2010.- [33] M. Takaki, D. Cavalcanti, R. Gheyi, J. Iyoda, M. D'Amorim, and R.B. Prudêncio, "Randomized Constraint Solvers: A Comparative Study,"
Innovation in Systems and Software Eng., vol. 6, pp. 243-253, Sept. 2010.- [34] C. Jard and T. Jéron, "TGV: Theory, Principles and Algorithms: A Tool for the Automatic Synthesis of Conformance Test Cases for Non-Deterministic Reactive Systems,"
Int'l J. Software Tools Technology Transfer, vol. 7, no. 4, pp. 297-315, 2005.- [35] W.L. Andrade and P.D.L. Machado, "Modeling and Testing Interruptions in Reactive Systems Using Symbolic Models,"
Proc. Second Brazilian Workshop Systematic and Automated Software Testing, pp. 34-43, 2008.- [36] I. Sommerville,
Software Engineering, ninth ed. Addison-Wesley, 2010.- [37] W.L. Andrade, D.R. Almeida, J.B. Cândido, and P.D.L. Machado, "SYMBOLRT: A Tool for Symbolic Model-Based Test Case Generation for Real-Time Systems,"
Proc. 19th Tools Session of the Third Brazilian Conf. Software: Theory and Practice, pp. 31-37, 2012.- [38] W.L. Andrade and P.D.L. Machado, "Testing Interruptions in Reactive Systems,"
Formal Aspects of Computing, vol. 24, pp. 331-353, 2012. |