maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-6-45-56mais-138Research ArticleОригинальные статьиArticlesКак разработать простое средство верификации систем реального времениOn the Designing of Model Checkers for Real-Time Distributed SystemsВолкановДмитрий ЮрьевичVolkanovD. Yu.

ассистент

ассистент

valdus@yandex.ruЗахаровВладимир АнатольевичZakharovV. A.

доцент

доцент

valdus@yandex.ruЗоринДаниил АлександровичZorinD. A.

аспирант

аспирант

valdus@yandex.ruКонновИгорь ВладимировичKonnovI. V.

ассистент

ассистент

ПодымовВладислав ВасильевичPodymovV. V.

аспирант

аспирант

valdus@yandex.ruМосковский государственный университет им. М.В. ЛомоносоваРоссияМосковский государственный университет им. М.В. ЛомоносоваRussian FederationВенский технологический университетАвстрияTechnische Universit¨at WienAustria2012120320151964556Copyright © Волканов Д.Ю., Захаров В.А., Зорин Д.А., Коннов И.В., Подымов В.В., 20152015Волканов Д.Ю., Захаров В.А., Зорин Д.А., Коннов И.В., Подымов В.В.Volkanov D.Y., Zakharov V.A., Zorin D.A., Konnov I.V., Podymov V.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/138

Исследуется задача верификации систем реального времени (СРВ). Для описания СРВ удобно использовать диаграммы состояний UML с семантикой, определяемой иерархическими автоматами. Для верификации СРВ часто применяется средство UPPAAL, разработанное для проверки формул логики TCTL на сети временных автоматов. Основным результатом данной статьи является алгоритм трансляции иерархических автоматов в сеть временных автоматов и обоснование его корректности.

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.

верификациясистема реального временидиаграмма состоянийиерархический автоматвременной автоматverificationreal time systemsstatechartshierarchical automatontimed automatonМинобрнауки РФ, федеральная целевая программа "Научные и научно-педагогические кадры инновационной России"ReferencesDavid A., Moller M.O. From HUppaal to Uppaal: a translation from hierarchical timed automata to flat timed automata // Research Series RS-01-11, BRICS, Department of Computer Science, University of Aarhus, March 2001.David A., Moller M.O. From HUppaal to Uppaal: a translation from hierarchical timed automata to flat timed automata // Research Series RS-01-11, BRICS, Department of Computer Science, University of Aarhus, March 2001.Lakhnech M.E., Siegal M. Hierarchical automata as model for statechart // Lecture Notes in Computer Science. 1997. V. 1345. P. 187–196.Lakhnech M.E., Siegal M. Hierarchical automata as model for statechart // Lecture Notes in Computer Science. 1997. V. 1345. P. 187–196.Chen Hai-yan, Dong Wei, Wang Huo-wang. Verify UML statechart with SMV // Wuhan University Journal of Natural Science. 2001. V. 6, №1–2. P. 183–190.Chen Hai-yan, Dong Wei, Wang Huo-wang. Verify UML statechart with SMV // Wuhan University Journal of Natural Science. 2001. V. 6, №1–2. P. 183–190.Jussila T., Dubrovin J., Junttila T., Latvala T., Pores I. Model checking dynamic and hierarchical UML state machines // Proc. of the 3rd Workshop on Model Design and Validation. 2006.Jussila T., Dubrovin J., Junttila T., Latvala T., Pores I. Model checking dynamic and hierarchical UML state machines // Proc. of the 3rd Workshop on Model Design and Validation. 2006.Latella D., Majzik I., Massink M. Automatic verification of a behavioural subset of UML statechart diagrams using SPIN model-checker // Formal Aspects of Computations. 1999. V. 11.Latella D., Majzik I., Massink M. Automatic verification of a behavioural subset of UML statechart diagrams using SPIN model-checker // Formal Aspects of Computations. 1999. V. 11.Lilius J., Paltor I. vUML: a Tool for Verifying UML Models // Technical Report TUCS-272. Turku Centre for Computer Science. 1999.Lilius J., Paltor I. vUML: a Tool for Verifying UML Models // Technical Report TUCS-272. Turku Centre for Computer Science. 1999.Ober I., Graf S., Ober I. Validating timed UML models by simulation and verification // Proc. of the Workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003). 2003.Ober I., Graf S., Ober I. Validating timed UML models by simulation and verification // Proc. of the Workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003). 2003.Behrmann G., David A., Larsen K.G. A Tutorial on Uppaal // Lecture Notes in Computer Science. 2004. V. 3185. P. 200–236.Behrmann G., David A., Larsen K.G. A Tutorial on Uppaal // Lecture Notes in Computer Science. 2004. V. 3185. P. 200–236.Bengtsson J., Larsen K.G., Larsson F., Pettersson P., Yi W. UPPAAL – a Tool Suite for Automatic Verification of Real-Time Systems // Lecture Notes in Computer Science. 1996. V. 1066. P. 232–243.Bengtsson J., Larsen K.G., Larsson F., Pettersson P., Yi W. UPPAAL – a Tool Suite for Automatic Verification of Real-Time Systems // Lecture Notes in Computer Science. 1996. V. 1066. P. 232–243.David A., Moller M.O., Yi W. Verification of UML statechart with real-time extensions // IT Tech. Rep. 2003-009, Uppsala: Dep. of Information Technology, Uppsala University. 2003.David A., Moller M.O., Yi W. Verification of UML statechart with real-time extensions // IT Tech. Rep. 2003-009, Uppsala: Dep. of Information Technology, Uppsala University. 2003.Muniz A.L.N., Andrade A.M.S., Lima G. Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems // Innovation in Software and System Engineering. 2009.Muniz A.L.N., Andrade A.M.S., Lima G. Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems // Innovation in Software and System Engineering. 2009.Alur R., Dill D.L. Automata for modeling real-time systems // Lecture Notes in Computer Science. 1990. V. 443/1990. P. 322–335.Alur R., Dill D.L. Automata for modeling real-time systems // Lecture Notes in Computer Science. 1990. V. 443/1990. P. 322–335.Alur R., Dill D.L. A theory of timed automata // Theoretical Computer Science. 1994. V. 126. P. 183–235.Alur R., Dill D.L. A theory of timed automata // Theoretical Computer Science. 1994. V. 126. P. 183–235.Browne M.C., Clarke M.C., Grumberg O. Characterizing finite Kripke structures in propo-sitional temporal logics // Theoretical Computer Science. 1988. V. 59 (1–2). P. 115–131.Browne M.C., Clarke M.C., Grumberg O. Characterizing finite Kripke structures in propo-sitional temporal logics // Theoretical Computer Science. 1988. V. 59 (1–2). P. 115–131.Chistolinov M.V., Epatko I.V., Bahmurov A.G., Smelyansky R.L., Zakharov V.A., Winter K., Usenko Y. Towards a unified toolset for embedded systems development // Proc. of the conference UKRPROG-2000 «Problems of Programming». 2000. №1–2. P. 316–322.Chistolinov M.V., Epatko I.V., Bahmurov A.G., Smelyansky R.L., Zakharov V.A., Winter K., Usenko Y. Towards a unified toolset for embedded systems development // Proc. of the conference UKRPROG-2000 «Problems of Programming». 2000. №1–2. P. 316–322.

The authors declare that there are no conflicts of interest present.