Abstract
The paper presents methods and algorithms for automatic design of test cases from the formal models of transition systems. Certain specific extended data flow coverage criteria are used as a test goal targets. Particular attention is paid to the problem of infeasible coverage targets, which in fact are unreachable, nevertheless are required for static analysis. Such cases interfere with statistics and make it difficult to measure the completeness of the coverage results obtained. We describe a method for specifying data flow chains and propose algorithms that combine dynamic refinement of the coverage targets with the search for paths satisfying them. In many practical cases, our approach achieves a combinatorial reduction in the number of coverage targets and, if the algorithm is successfully terminated, the completeness of the desired coverage.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Odarushchenko O., et al.: Application of formal verification methods in a safety-oriented software development life cycle. In: 13th International Conference on Dependable Systems, Services and Technologies, pp. 1–6 (2023). https://doi.org/10.1109/DESSERT61349.2023.10416448
Paul, S., et al.: Formal verification of safety-critical aerospace systems. IEEE Aeros. Electron. Syst. Mag. 38(5), 72–88 (2023)
Fremont, D., et al.: Formal scenario-based testing of autonomous vehicles: from simulation to the real world. In: IEEE 23rd International Conference on Intelligent Transportation Systems, pp. 1–8 (2020). https://doi.org/10.1109/ITSC45102.2020.9294368
Liu, S., Nakajima, S.: Automatic test case and test oracle generation based on functional scenarios in formal specifications for conformance testing. IEEE Trans. Softw. Eng. 48(2), 691–712 (2022). https://doi.org/10.1109/TSE.2020.2999884
Weigert, T., et al.: Generating test suites to validate legacy systems. In: Fonseca i Casas, P., Sancho, MR., Sherratt, E. (eds.) SAM 2019. Lecture Notes in Computer Science, vol. 11753, pp. 3–23. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30690-8_1
Gay, G., Staats, M., Whalen, M., Heimdahl, M.: The risks of coverage-directed test case generation. IEEE Trans. Softw. Eng. 41, 803–819 (2015)
Kolchin, A., Potiyenko, S.: Extending data flow coverage to test constraint refinements. In: ter Beek, M.H., Monahan, R. (eds.) Integrated formal methods. IFM 2022. Lecture Notes in Computer Science, vol. 13274. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-07727-2_17
Kolchin, A., Potiyenko, S., Weigert, T.: Extending data flow coverage with redefinition analysis. In: IEEE International Conference on Information and Digital Technologies (IDT), Zilina, Slovakia, pp. 293–296 (2021). https://doi.org/10.1109/IDT52577.2021.9497535
Su, T., Ke, W., Miao, W., et al.: A survey on data-flow testing. ACM Comput. Surv. 50, 35 (2017)
Rapps, S., Weyuker, E.: Data flow analysis techniques for test data selection. In: Proceedings of International Conference of Software Engineering, pp. 272–277 (1982)
Ntafos, S.: On required element testing. IEEE Trans. Softw. Eng. 10, 795–803 (1984)
Hong, H., Ural, H.: Dependence testing: extending data flow testing with control dependence. In: Khendek, F., Dssouli, R. (eds.) Testing of Communicating Systems. Lecture Notes in Computer Science, vol. 3502. Springer, Cham (2005). https://doi.org/10.1007/11430230_3
Su, T., et al.: Combining symbolic execution and model checking for data flow testing. In: IEEE/ACM 37th IEEE International Conference on Software Engineering, pp. 654–665 (2015). https://doi.org/10.1109/ICSE.2015.81
Martin, T., Kosmatov, N., Prevosto, V., Lemerre, M.: Detection of polluting test objectives for dataflow criteria. In: Dongol, B., Troubitsyna, E. (eds.) Integrated Formal Methods. IFM 2020. Lecture Notes in Computer Science, vol. 12546. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63461-2_18
Marashdih, A., Zaaba, Z., Almufti, S.: The problems and challenges of infeasible paths in static analysis. Int. J. Eng. Technol. 7(4.19), 412–417 (2018)
Lange, T., Neuhäußer, M.R., Noll, T., et al.: IC3 software model checking. Int. J. Softw. Tools Technol. Transf. 22, 135–161 (2020). https://doi.org/10.1007/s10009-019-00547-x
Hessel, A., Petterson, P.: A global algorithm for model-based test suite generation. Electr. Notes Theor. Comput. Sci. 190, 47–59 (2007)
Su, T., et al.: Towards efficient data-flow test data generation. In: Bowen, J.P., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol. 14080. Springer, Cham (2023)
Dssouli, R., Khoumsi, A., et al.: Testing the control-flow, data-flow, and time aspects of communication systems: a survey. Adv. Comput. 107, 95–155 (2017)
Trabish, D., Mattavelli, A., Cadar, C.: Chopped symbolic execution. In: Proceedings of ICSE 2018, pp. 350–360 (2018). https://doi.org/10.1145/3180155.3180251
Beyer, D., Gulwani, S., Schmidt, D.: Combining Model Checking and Dataflow Analysis. Handbook of Model Checking, pp. 493–540. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8
Kolchin A.: A novel algorithm for attacking path explosion in model-based test generation for data flow coverage. In: Proceedings of IEEE 1st International Conference on System Analysis and Intelligent Computing, SAIC, pp. 226–231 (2018). https://doi.org/10.1109/SAIC.2018.8516824
Boonstoppel, P., Cadar, C., Engler, D.: RWset: attacking path explosion in constraint-based test generation. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 351–366. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-327
Kolchin, A.V.: An automatic method for the dynamic construction of abstractions of states of a formal model. Cybernet. Syst. Anal. 46(4), 583–601 (2010). https://doi.org/10.1007/s10559-010-9235-9
Gallardo, M.M., Merino, P., Panizo, L.: The role of abstraction in model checking. In: Lopez-Garcia, P., Gallagher, J.P., Giacobazzi, R. (eds.) Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems. Lecture Notes in Computer Science, vol. 13160. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-31476-6_8
Mariano, M., et al.: Comparing graph-based algorithms to generate test cases from finite state machines. J. Electron. Test. 35, 867–885 (2019). https://doi.org/10.1007/s10836-019-05844-6
Yadzhak, M.: Parallel algorithms for data digital filtering. Cybernet. Syst. Anal. 59, 39–48 (2023). https://doi.org/10.1007/s10559-023-00540-y
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Kolchyn, O., Potiyenko, S. (2024). Model-Based Test Cases Generation for Extended Data Flow Coverage Criteria. In: Silhavy, R., Silhavy, P. (eds) Software Engineering Methods Design and Application. CSOC 2024. Lecture Notes in Networks and Systems, vol 1118. Springer, Cham. https://doi.org/10.1007/978-3-031-70285-3_43
Download citation
DOI: https://doi.org/10.1007/978-3-031-70285-3_43
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-70284-6
Online ISBN: 978-3-031-70285-3
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)