Verification of Quantitative Temporal Properties in RealTime-DEVS
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913781004632064 |
|---|---|
| author | González, Ariel Cristiá, Maximiliano Luna, Carlos |
| author_facet | González, Ariel Cristiá, Maximiliano Luna, Carlos |
| contents | Real-Time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify that kind of temporal properties requires to use something beyond simulation. In this work we use the model checker Uppaal to verify a class of recurrent quantitative temporal properties appearing in RT-DEVS models, even though Uppaal cannot deal in general with this kind of properties. In order to overcome these limitations we use the technique known as automata observer. Secondly, by introducing mutations to quantitative temporal properties we are able to find errors in RT-DEVS models and their implementations. A case study from the railway domain is presented. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_18732 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Verification of Quantitative Temporal Properties in RealTime-DEVS González, Ariel Cristiá, Maximiliano Luna, Carlos Software Engineering Real-Time DEVS (RT-DEVS) can model systems with quantitative temporal requirements. Ensuring that such models verify that kind of temporal properties requires to use something beyond simulation. In this work we use the model checker Uppaal to verify a class of recurrent quantitative temporal properties appearing in RT-DEVS models, even though Uppaal cannot deal in general with this kind of properties. In order to overcome these limitations we use the technique known as automata observer. Secondly, by introducing mutations to quantitative temporal properties we are able to find errors in RT-DEVS models and their implementations. A case study from the railway domain is presented. |
| title | Verification of Quantitative Temporal Properties in RealTime-DEVS |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2409.18732 |