Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation
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_ | 1866916147580895232 |
|---|---|
| author | Mahe, Erwan Bannour, Boutheina Gaston, Christophe Lapitre, Arnault Gall, Pascale Le |
| author_facet | Mahe, Erwan Bannour, Boutheina Gaston, Christophe Lapitre, Arnault Gall, Pascale Le |
| contents | Offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces, given the absence of a global clock. To account for this, we model executions as collections of local traces called multi-traces, with one local trace per group of co-localized actors that share a common clock. Due to the difficulty of synchronizing the start and end of the recordings of local traces, events may be missing at their beginning or end. Considering such partially observed multi-traces is challenging for runtime verification. To that end, we propose an algorithm that verifies the conformity of such traces against formal specifications called Interactions (akin to Message Sequence Charts). It relies on parameterized simulation to reconstitute unobserved behaviors. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_03083 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation Mahe, Erwan Bannour, Boutheina Gaston, Christophe Lapitre, Arnault Gall, Pascale Le Software Engineering Offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces, given the absence of a global clock. To account for this, we model executions as collections of local traces called multi-traces, with one local trace per group of co-localized actors that share a common clock. Due to the difficulty of synchronizing the start and end of the recordings of local traces, events may be missing at their beginning or end. Considering such partially observed multi-traces is challenging for runtime verification. To that end, we propose an algorithm that verifies the conformity of such traces against formal specifications called Interactions (akin to Message Sequence Charts). It relies on parameterized simulation to reconstitute unobserved behaviors. |
| title | Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2403.03083 |