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

被引：0

作者：

Konnov I.V. ^{[2
]}

Podymov V.V. ^{[1
]}

Volkanov D.Y. ^{[1
]}

Zakharov V.A. ^{[1
]}

Zorin D.A. ^{[1
]}

机构：

[1] Lomonosov Moscow State University, Moscow

[2] Technische Universität Wien, Wien

来源：

Automatic Control and Computer Sciences | 2014年 / 48卷 / 07期

关键词：

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

D O I：

10.3103/S0146411614070232

中图分类号：

学科分类号：

摘要：

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. © 2014, Allerton Press, Inc.

引用

页码：534 / 542

页数：8

共 15 条

[1]

David A., Moller M.O., From HUppaal to Uppaal: a translation from hierarchical timed automata to flat timed automata, (2001)

[2]

Lakhnech M.E., Siegal M., Hierarchical automata as model for statechart, Lecture Notes Compt. Sci., 1345, pp. 187-196, (1997)

[3]

Chen H.-Y., Dong W., Wang H.-W., Verify UML statechart with SMV, Wuhan Univ. J. Natur. Sci., 6, pp. 183-190, (2001)

[4]

Jussila J., Dubrovin T., Junttila T., Latvala I., Pores. Model checking dynamic and hierarchical UML state machines, Proc, 3rd Workshop on Model Design and Validation, (2006)

[5]

Latella D., Majzik I., Massink M., Automatic verification of a behavioral subset of UML statechart diagrams using SPIN model-checker, Formal Aspects Compt., 11, pp. 637-664, (1999)

[6]

Lilius J., Paltor I., vUML: A Tool for Verifying UML Models, (1999)

[7]

Ober I., Graf S., Ober I., Validating timed UML models by simulation and verification, Proc, Workshop on Specification and Validation of UML Models for Real Time and Embedded Systems, (2003)

[8]

Behrmann G., David A., Larsen K.G., A tutorial on Uppaal, Lecture Notes in Compt. Sci., 3185, pp. 200-236, (2004)

[9]

Bengtsson G., Larsen K.G., Larsson F., Pettersson P., Yi W., UPPAAL — a tool suite for automatic verification of real-time systems, Lecture Notes in Compt. Sci., 1066, pp. 232-243, (1996)

[10]

David A., Moller M.O., Yi W., Verification of UML Statechart with Real-Time Extensions, (2003)

← 1 2 →