Name
Abstract | ||
|---|---|---|
The mission- and life-critical properties of distributed real-time systems require concurrent modeling, analysis, and formal verification in the design stage. The timed input/output automata (TIOA) framework and the UPPAAL software package are two widely used modeling and verification tools for this purpose. To this end, we develop the algorithm TUConvert for converting distributed TIOA models to UPPAAL behavioral models and formally prove its correctness. We demonstrate the applicability of our algorithm by the formal verification of a distributed real-time industrial communication protocol that is modeled by TIOA. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2964202 | ACM Trans. Embedded Comput. Syst. |
Keywords | Field | DocType |
Distributed real-time systems,timed input/output automata,UPPAAL,formal verification | Programming language,Computer science,Automaton,Correctness,Industrial communication,Real-time computing,Software,Distributed computing,Formal verification | Journal |
Volume | Issue | ISSN |
16 | 1 | 1539-9087 |
Citations | PageRank | References |
1 | 0.39 | 26 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yusuf Bora Kartal | 1 | 1 | 0.72 |
| Ece Guran Schmidt | 2 | 146 | 16.27 |
| Klaus Werner Schmidt | 3 | 166 | 20.90 |
| KartalYusuf Bora | 4 | 1 | 0.39 |
| SchmidtEce GÜran | 5 | 1 | 0.39 |
| SchmidtKlaus Werner | 6 | 1 | 0.39 |