Translation of Timed Promela to Timed Automata with Discrete Data

被引：0

作者：

Nabialek, Wojciech ^{[1
]}

Janowska, Agata ^{[2
]}

Janowski, Pawel ^{[2
]}

机构：

[1] Univ Podlasie, Inst Comp Sci, PL-08110 Siedlce, Poland

[2] Univ Warsaw, Inst Informat, PL-02097 Warsaw, Poland

来源：

FUNDAMENTA INFORMATICAE | 2008年 / 85卷 / 1-4期

关键词：

Promela; Spin; Timed Automata; timed systems; model checking;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The aim of the work is twofold. In order to face the problem of modeling time constraints in Promela. a timed extension of the language is presented. Next, timed Promela is translated to timed automata with discrete data, that is timed automata extended with integer variables. The translation enables verification of Promela specifications via tools accepting timed automata as input, such as VerICS or Uppaal. The translation is illustrated with a well known example of Fischer's mutual exclusion protocol. Some experimental results are also presented.

引用

页码：409 / 424

页数：16

共 12 条

[1] ALUR R, 1990, LECT NOTES COMPUT SC, V443, P322, DOI 10.1007/BFb0032042
[2] ALUR R, 1992, REAL-TIME SYSTEMS SYMPOSIUM : PROCEEDINGS, P157, DOI 10.1109/REAL.1992.242667
[3] Bengtsson J., 1998, P INT WORKSH SOFTW T
[4] Bosnacki D, 1998, LECT NOTES COMPUT SC, V1486, P307, DOI 10.1007/BFb0055359
[5] Cimatti A., 2002, LNCS, P359, DOI [10.1007/3-540-45657-0_29, DOI 10.1007/3-540-45657-0_29]
[6] Daws C., 1995, HYBRID SYSTEMS 3 VER, P208, DOI DOI 10.1007/BFB0020947
[7] Dembinski P, 2003, LECT NOTES COMPUT SC, V2619, P278
[8] HyTech: A model checker for hybrid systems
Henzinger T.A.
Ho P.-H.
Wong-Toi H.
[J]. International Journal on Software Tools for Technology Transfer, 1997, 1 (1-2) : 110 - 122
[9] Holzmann G., 2003, The SPIN Model Checker-Primer and Reference (M)anual
[10] Janowska A, 2006, FUND INFORM, V72, P181

← 1 2 →