Modeling Distributed Real-Time Systems in TIOA and UPPAAL


Kartal Y. B. , SCHMİDT Ş. E. , SCHMİDT K. W.

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, cilt.16, 2016 (SCI İndekslerine Giren Dergi) identifier identifier

  • Cilt numarası: 16 Konu: 1
  • Basım Tarihi: 2016
  • Doi Numarası: 10.1145/2964202
  • Dergi Adı: ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS

Özet

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.