Aplicando paralelismo a un algoritmo de bisimulación para mejorar la eficiencia de pruebas de software de sistemas de tiempo crítico
Barra lateral del artículo
Contenido principal del artículo
Los Sistemas de Tiempo Crítico (STC) son importantes cuando estrictos requerimientos temporales garantizan fiabilidad y correctitud de los sistemas. Las Pruebas de Mutación (PM) son una valiosa técnica para el aseguramiento de la calidad de STCs, pero sufren del Problema de los Mutantes Equivalentes (PME), que incrementa costos de cómputo y reduce la confiabilidad de PM. Para combatir el PME, un algoritmo de Bisimulación Temporizada (BT) puede ser usado si los STC se expresan como Autómatas de Tiempo (AT). BT es computacionalmente costoso, y podría beneficiarse de técnicas de paralelismo. En este trabajo, se analizan implementaciones de BT disponibles en la literatura, se identifican oportunidades para aplicar técnicas de paralelismo, se construye una solución que aprovecha estas oportunidades, y se comprueba su efectividad. La solución construida es un programa en Java que recibe múltiples ATs en formato UPPAAL y determina qué ATs son equivalentes, usando una implementación de BT como TimBrCheck o MUTES y paralelismo basado en procesos. Comparado con las soluciones disponibles previamente, los experimentos muestran que nuestra propuesta es más eficiente, ya que los tiempos de ejecución de BT se reducen a menos de la mitad. Esto podría mejorar el alcance, la confiabilidad y efectividad de PM para STC.
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
Aceptado 2023-08-23
Publicado 2023-11-29
Esta obra está bajo una licencia internacional Creative Commons Atribución-NoComercial-CompartirIgual 4.0.
Los autores que publican en esta revista están de acuerdo con los siguientes términos:
- Los autores conservan los derechos de autor y garantizan a la revista el derecho de ser la primera publicación del trabajo al igual que licenciado bajo una Creative Commons Attribution License que permite a otros compartir el trabajo con un reconocimiento de la autoría del trabajo y la publicación inicial en esta revista. A partir del volumen 22 número 1 (2020), la revista adopta la licencia CC BY-NC-SA 4.0.
- Los autores pueden establecer por separado acuerdos adicionales para la distribución no exclusiva de la versión de la obra publicada en la revista (por ejemplo, situarlo en un repositorio institucional o publicarlo en un libro), con un reconocimiento de su publicación inicial en esta revista.
- Se permite y se anima a los autores a difundir sus trabajos electrónicamente (por ejemplo, en repositorios institucionales o en su propio sitio web) antes y durante el proceso de envío, ya que puede dar lugar a intercambios productivos, así como a una citación más temprana y mayor de los trabajos publicados.