How to make a simple tool for verification of real-time systems.

Authors

Konnov I.V., Podymov V.V., Volkanov D.Yu, Zorin D.A., Zakharov V.A.

Abstract

To verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.

Text of article

Keywords

verification, real time systems, statecharts, hierarchical automaton, timed automaton, Computational Tree Logic

Edition

Automatic Control and Computer Sciences, Allerton Press Inc. (United States), 2014, vol 48, № 7, pp. 534-542.

Research Group

Theoretical Computer Science

All publications during 2014

All publications