Applying parallelism to a bisimulation algorithm to improve efficiency in software testing of time-critical systems
Article Sidebar
Main Article Content
Time-Critical Systems (TCS) play a crucial role in environments where strict timing constraints are essential to ensure reliability and correctness. Mutation Testing (MT) is considered a valuable strategy for quality assurance of TCS, but it suffers from the equivalent mutant problem, which is known to increase computational cost and reduce confidence in MT. To address this problem, a strong timed bisimulation equivalence (STBE) algorithm can be used when TCS are modeled as Timed Automata (TA). STBE is computationally expensive and can benefit from parallelism. We survey available STBE implementations, identify opportunities to apply parallelism, build an extension that takes advantage of them, and test its effects. The resulting solution is a Java program that receives multiple TAs expressed in UPPAAL format and determines which TAs are equivalent using an STBE implementation such as TimBrCheck or MUTES and process-based parallelism. Compared to existing solutions, our tests show that our proposal is more efficient, reducing the runtimes of STBE by more than half. This could improve the reach, reliability, and effectiveness of MT for TCS.
Tretmans, J. Model Based Testing with Labeled Transition Systems. In: Formal Methods and Testing – An Outcome of the FORTEST Network. Berlin: Springer-Verlag, 2008. p. 1–38. DOI: https://doi.org/10.1007/978-3-540-78917-8_1
Zander, J, Schieferdecker, I. Model-Based Testing for Embedded Systems. CRC Press; 2017. DOI: https://doi.org/10.1201/b11321
Budd, TA, Gopal, AS. “Program testing by specification mutation”. Computer Languages, 1985. DOI: https://doi.org/10.1016/0096-0551(85)90011-6
Jia, Y, Harman, M. “An Analysis and Survey of the Development of Mutation Testing”. IEEE Transactions on Software Engineering 2011; 37(5):649-678. DOI: https://doi.org/10.1109/TSE.2010.62
Papadakis, M, Kintis, M, Zhang, J, Yue, Traon, Y, Harman, M. Chapter Six - Mutation Testing Advances: An Analysis and Survey. In: Advances in Computers, Volume 112, 2019; 112:275-378. DOI: https://doi.org/10.1016/bs.adcom.2018.03.015
Ortiz Vega, J, Perrouin, G, Amrani, M, Schobbens, PY. Model-Based Mutation Operators for Timed Systems: A Taxonomy and Research Agenda. In 2018 IEEE International Conference on Software Quality, Reliability and Security (QRS) 2018 (pp. 325-332). DOI: https://doi.org/10.1109/QRS.2018.00045
Guha, S. On Decidability of Prebisimulation for Timed Automata. In Computer Aided Verification, 2012 (pp. 444–461). Springer Berlin Heidelberg. DOI: https://doi.org/10.1007/978-3-642-31424-7_33
Leiserson, CE, Thompson, NC, Emer, JS, Kuszmaul, BC, Lampson, BW, Sanchez, D, Schardl, TB. “There’s plenty of room at the Top: What will drive computer performance after Moore’s law?”. Science 2020; 368(6495):eaam9744. DOI: https://doi.org/10.1126/science.aam9744
Luthmann, L, Göttmann, H, Bacher, I, Lochau, M. Checking Timed Bisimulation with Bounded Zone-History Graphs – Technical Report. 2019. Available at: https://arxiv.org/abs/1910.08992
Ortiz Vega, J, Amrani, M, Schobbens, PY. Multi-timed Bisimulation for Distributed Timed Automata. In NASA Formal Methods, 2017 (pp. 52–67). Springer International Publishing. DOI: https://doi.org/10.1007/978-3-319-57288-8_4
Baier, C, Katoen, JP. Principles of Model Checking. The MIT Press; 2008. pp. 673-738
Čerāns, K. Decidability of bisimulation equivalences for parallel timer processes. In Computer Aided Verification, 1993 (pp. 302–315). Springer Berlin Heidelberg. DOI: https://doi.org/10.1007/3-540-56496-9_24
UPPAAL [Internet]. Uppsala Universitet. Available at: https://uppaal.org/
Weise, C, Lenzkens, D. Efficient scaling-invariant checking of timed bisimulation. In STACS 97 1997 (pp. 177–188). Springer Berlin Heidelberg. DOI: https://doi.org/10.1007/BFb0023458
Concurrency Workbench of the New Century [Internet]. North Carolina State University; [cited Aug 13 2023]. Available at: https://www3.cs.stonybrook.edu/~cwb/
Andersen, J, Hansen, M, Andersen, N. CAAL [Internet]. Aalborg University; [cited Aug 13 2023]. Available at: http://caal.cs.aau.dk/docs/CAAL2_EPG.pdf
Kanellakis P. Smolka S. “CCS expressions, finite state processes, and three problems of equivalence”. Information and Computation, 1990. DOI: https://doi.org/10.1016/0890-5401(90)90025-D
R. Paige, R. Tarjan. “Three partition refinement algorithms”. SIAM Journal on Computing 1987. DOI: https://doi.org/10.1137/0216062
Martens J, Groote, JF, van den Haak, LB, Hijma, P, Wijs, A. “A linear parallel algorithm to compute bisimulation and relational coarsest partitions”. CoRR 2021; abs/2105.11788. DOI: https://doi.org/10.1007/978-3-030-90636-8_7
ANTRL [Internet]. Available at: https://www.antlr.org/
Betancourt JS. A parallel algorithm to compute strong timed bisimulation [bachelor’s thesis]. Cali: Universidad del Valle; 2023 [cited Aug 10 2023]. Available at: https://drive.google.com/file/d/1zxDyAf-4qXV0tMry8MkbTThjzJKBUr5b/view?usp=sharing
Lindahl, W. Formal design and analysis of a gear controller. In Tools and Algorithms for the Construction and Analysis of Systems, 1998 (pp. 281–297). Springer Berlin Heidelberg.
Jensen, H, Larsen, K, Skou, A. “Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL”. BRICS Report Series 2002; 3. DOI: https://doi.org/10.7146/brics.v3i24.20005
Lindahl, M, Tettersson, P, Yi W. Formal design and analysis of a gear controller. In Tools and Algorithms for the Construction and Analysis of Systems, 1998. Springer Berlin Heidelberg. DOI: https://doi.org/10.1007/BFb0054178
Basile, D, Beek, M, Cordy, M, Legay, A. Tackling the Equivalent Mutant Problem in Real-Time Systems: The 12 Commandments of Model-Based Mutation Testing. In Proceedings of the 24th ACM Conference on Systems and Software Product Line: Volume A - Volume A 2020. Association for Computing Machinery. DOI: https://doi.org/10.1145/3382025.3414966
Cuartas, J, Aranda, J, Cordy, M, Ortiz, J, Perrouin, G, Schobbens, PY. MUPPAAL: Reducing and Removing Equivalent and Duplicate Mutants in UPPAAL. In 2023 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW) 2023. DOI: https://doi.org/10.1109/ICSTW58534.2023.00021
Oracle. Thread (Java Platform SE7). [Cited Aug 14 2023] Available at https://docs.oracle.com/javase/7/docs/api/java/lang/Thread.html
Basile D, Alessandro Fantechi, Rosadi I. Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer. Lecture Notes in Computer Science. 2021 Jan 1;174–90. DOI: https://doi.org/10.1007/978-3-030-85248-1_11
Mercaldo, F, Martinelli, F, & Santone, A. Real-Time SCADA Attack Detection by Means of Formal Methods. In 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE) (pp. 231-236). DOI: https://doi.org/10.1109/WETICE.2019.00057
Guo, X, Lin, HH, Kenro, Yatake. An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol. Communications in computer and information science. 2014. DOI: https://doi.org/10.1007/978-3-319-05416-2_4
Pajic, M, Jiang, Z, Lee, I, Sokolsky, O, Mangharam, R. From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study. IEEE 18th Real Time and Embedded Technology and Applications Symposium 2012. DOI: https://doi.org/10.1109/RTAS.2012.25
Cuartas, J, Cortés, D, Betancourt, J, Aranda, J, García, J, Valencia, A, Ortiz, J. Formal Verification of a Mechanical Ventilator Using UPPAAL. In Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems 2023 (pp. 2–13). Association for Computing Machinery. DOI: https://doi.org/10.1145/3623503.3623536
Lorber, F, Larsen, K, Nielsen, BModel-Based Mutation Testing of Real-Time Systems via Model Checking. In 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW) 2018 (pp. 59-68). DOI: https://doi.org/10.1109/ICSTW.2018.00029
Larsson, J. Automatic Test Generation and Mutation Analysis using UPPAAL SMC [Thesis]. Marinescu R, editor. [Mälardalen University, School of Innovation, Design and Engineering]; 2017.
Siavashi, J. Testing Web Services with Model-Based Mutation. In Software Technologies 2017 (pp. 45–67). Springer International Publishing. DOI: https://doi.org/10.1007/978-3-319-62569-0_3
Mathematical program solvers - IBM CPLEX [Internet]. Ibm.com. Available from: https://www.ibm.com/products/ilog-cplex-optimization-studio/cplex-optimizer
Accepted 2023-08-23
Published 2023-09-08
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Authors grant the journal and Universidad del Valle the economic rights over accepted manuscripts, but may make any reuse they deem appropriate for professional, educational, academic or scientific reasons, in accordance with the terms of the license granted by the journal to all its articles.
Articles will be published under the Creative Commons 4.0 BY-NC-SA licence (Attribution-NonCommercial-ShareAlike).