Metodología de verificación, detección de errores y generación de casos de prueba en modelos RT-DEVS con requisitos temporales cuantitativos

Abstract

Los sistemas de tiempo real suelen presentar errores vinculados a la temporización que son difíciles de detectar. Los formalismos utilizados para modelar este tipo de sistemas permiten especificar comportamientos a diferentes niveles de abstracción, descomponiendo los modelos en submodelos (componentes), los cuales interactúan entre sí para describir correctamente el comportamiento global del sistema. Los requisitos temporales cuantitativos añaden una complejidad adicional a estos modelos, que pueden inducir a los diseñadores a cometer errores, especialmente en aspectos temporales durante la construcción. En sistemas grandes, el número de componentes suele ser considerable, por lo que es necesario contar con herramientas que automaticen la tarea de verificar si el modelo cumple con los requisitos del problema. DEVS (Discrete Event System Specification) es un formalismo matemático utilizado para modelar sistemas dinámicos discretos, especialmente aquellos que evolucionan a lo largo del tiempo debido a eventos que ocurren en momentos específicos. Estos modelos, y en particular los de la variante RealTime-DEVS (RT-DEVS), permiten especificar sistemas con requisitos temporales cuantitativos, pero carecen de un mecanismo de verificación formal (model checkers, SAT Solvers, etc.) que posibilite la comprobación de este tipo de requisitos. En esta tesis se propone un mecanismo que, por un lado, permite verificar con un model checker si los modelos RT-DEVS cumplen con un conjunto de propiedades recurrentes (patrones) en los sistemas, y por otro lado, basado en mutantes de propiedades temporales, ayuda a descubrir errores en los sistemas cuando no se satisfacen tales propiedades. En este trabajo, utilizamos el model checker Uppaal tanto para verificar un conjunto de patrones de propiedades temporales (Time-Bounded Response, Precedence with Delay, Time-Restricted Precedence, Conditional Security, Time-Bounded Frequency, entre otros), como para detectar errores de temporización mediante mutantes de dichos patrones en modelos RT-DEVS. Aunque Uppaal no admite directamente el análisis de estas propiedades, proponemos un proceso de transformaciones y empleamos la técnica del autómata observador para habilitar dicho análisis en Uppaal. Además, se define un mecanismo para generar casos de prueba a partir de los patrones y sus mutantes, que complementa las estrategias convencionales en la ingeniería de software. A lo largo del trabajo, se introduce y analiza un caso de estudio sobre un sistema de cruce de trenes.

Real-time systems often have timing-related errors that are hard to detect. The formalisms used to model these systems allow for the specification of behaviors at different levels of abstraction by decomposing models into submodels (components), which interact with one another to accurately describe the overall system behavior. Quantitative temporal requirements introduce additional complexity into these models, potentially causing engineers to introduce errors, particularly regarding timing aspects during development. In large-scale systems, the number of components tends to be substantial, hence the need for tools that automate the verification of models with respect to the system requirements. DEVS (Discrete Event System Specification) is a mathematical formalism used to model discrete dynamic systems, especially those that evolve over time due to events occurring at specific moments. These models, and in particular those of the Real-Time DEVS (RT-DEVS) variant, allow for the specification of systems with quantitative temporal requirements, but they lack a formal verification mechanism (model checkers, SAT solvers, etc.) to enable the validation of such requirements. In this thesis, a mechanism is proposed that, on one hand, allows verifying with a model checker whether RT-DEVS models satisfy a set of recurrent properties (patterns) in systems. On the other hand, based on temporal property mutants, helps to uncover errors in the systems when such properties are not satisfied. In this work, we use the model checker Uppaal both to verify a set of temporal property patterns (Time-Bounded Response, Precedence with Delay, Time-Restricted Precedence, Conditional Security, Time-Bounded Frequency, among others), and to detect timing errors through mutants of these patterns in RT-DEVS models. Even though, in general, Uppaal cannot handle this kind of properties, we propose a transformation process and employ the observer automaton technique to enable such analysis. Additionally, a mechanism is defined to generate test cases from the patterns and their mutants, complementing conventional strategies in software engineering. Throughout the work, a case study from the railway domain is introduced and analyzed.