Geodesic
On the Designing of Model Checkers for Real-Time Distributed Systems
Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 6, pp. 45-56

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: verification, real time systems, statecharts, hierarchical automaton, timed automaton. 
@article{MAIS_2012_19_6_a3,
     author = {D. Yu. Volkanov and V. A. Zakharov and D. A. Zorin and I. V. Konnov and V. V. Podymov},
     title = {On the {Designing} of {Model} {Checkers} for {Real-Time} {Distributed} {Systems}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {45--56},
     publisher = {mathdoc},
     volume = {19},
     number = {6},
     year = {2012},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a3/}
}
TY  - JOUR
AU  - D. Yu. Volkanov
AU  - V. A. Zakharov
AU  - D. A. Zorin
AU  - I. V. Konnov
AU  - V. V. Podymov
TI  - On the Designing of Model Checkers for Real-Time Distributed Systems
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2012
SP  - 45
EP  - 56
VL  - 19
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a3/
LA  - ru
ID  - MAIS_2012_19_6_a3
ER  - 
%0 Journal Article
%A D. Yu. Volkanov
%A V. A. Zakharov
%A D. A. Zorin
%A I. V. Konnov
%A V. V. Podymov
%T On the Designing of Model Checkers for Real-Time Distributed Systems
%J Modelirovanie i analiz informacionnyh sistem
%D 2012
%P 45-56
%V 19
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a3/
%G ru
%F MAIS_2012_19_6_a3
D. Yu. Volkanov; V. A. Zakharov; D. A. Zorin; I. V. Konnov; V. V. Podymov. On the Designing of Model Checkers for Real-Time Distributed Systems. Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 6, pp. 45-56. http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a3/