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...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2015-03-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/138 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849240794406322176 |
|---|---|
| author | D. Yu. Volkanov V. A. Zakharov D. A. Zorin I. V. Konnov V. V. Podymov |
| author_facet | D. Yu. Volkanov V. A. Zakharov D. A. Zorin I. V. Konnov V. V. Podymov |
| author_sort | D. Yu. Volkanov |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-41b86a8b67e748ee96fa18286abd520f |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2015-03-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-41b86a8b67e748ee96fa18286abd520f2025-08-20T04:00:26ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172015-03-01196455610.18255/1818-1015-2012-6-45-56132On the Designing of Model Checkers for Real-Time Distributed SystemsD. Yu. Volkanov0V. A. Zakharov1D. A. Zorin2I. V. Konnov3V. V. Podymov4Московский государственный университет им. М.В. ЛомоносоваМосковский государственный университет им. М.В. ЛомоносоваМосковский государственный университет им. М.В. ЛомоносоваTechnische Universit¨at WienМосковский государственный университет им. М.В. Ломоносова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.https://www.mais-journal.ru/jour/article/view/138verificationreal time systemsstatechartshierarchical automatontimed automaton |
| spellingShingle | 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 Моделирование и анализ информационных систем verification real time systems statecharts hierarchical automaton timed automaton |
| title | On the Designing of Model Checkers for Real-Time Distributed Systems |
| title_full | On the Designing of Model Checkers for Real-Time Distributed Systems |
| title_fullStr | On the Designing of Model Checkers for Real-Time Distributed Systems |
| title_full_unstemmed | On the Designing of Model Checkers for Real-Time Distributed Systems |
| title_short | On the Designing of Model Checkers for Real-Time Distributed Systems |
| title_sort | on the designing of model checkers for real time distributed systems |
| topic | verification real time systems statecharts hierarchical automaton timed automaton |
| url | https://www.mais-journal.ru/jour/article/view/138 |
| work_keys_str_mv | AT dyuvolkanov onthedesigningofmodelcheckersforrealtimedistributedsystems AT vazakharov onthedesigningofmodelcheckersforrealtimedistributedsystems AT dazorin onthedesigningofmodelcheckersforrealtimedistributedsystems AT ivkonnov onthedesigningofmodelcheckersforrealtimedistributedsystems AT vvpodymov onthedesigningofmodelcheckersforrealtimedistributedsystems |