Metodología de verificación, detección de errores y generación de casos de prueba en modelos RT-DEVS con requisitos temporales cuantitativos
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 (componen...
Saved in:
| Main Author: | |
|---|---|
| Format: | doctoralThesis |
| Language: | Spanish |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/20.500.12008/51727 |
| Tags: |
No Tags, Be the first to tag this record!
|
| Summary: | 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. |
|---|