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, sa.1, 2016 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 16 Sayı: 1
  • Basım Tarihi: 2016
  • Doi Numarası: 10.1145/2964202
  • Dergi Adı: ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus
  • Orta Doğu Teknik Üniversitesi Adresli: Evet

Ö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.