Modeling Distributed Real-Time Systems in Tioa and Uppaal

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.