On the Designing of Model Checkers for Real-Time Distributed Systems

On the Designing of Model Checkers for Real-Time Distributed Systems

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

Full description

Saved in:
Bibliographic Details
Main Authors: D. Yu. Volkanov, V. A. Zakharov, D. A. Zorin, I. V. Konnov, V. V. Podymov
Format: Article
Language:English
Published: Yaroslavl State University 2015-03-01
Series:Моделирование и анализ информационных систем
Subjects:
verification
real time systems
statecharts
hierarchical automaton
timed automaton
Online Access:https://www.mais-journal.ru/jour/article/view/138
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1818-1015
2313-5417

Similar Items