Affiliations: Institute of Computer Science, University of Podlasie,
ul. Sienkiewicza 51, 08-110 Siedlce, Poland. [email protected] | Institute of Informatics, University of Warsaw, Banacha
2, 02-097 Warsaw, Poland. {janowska, janowski}@mimuw.edu.pl
Note: [] Address for correspondence: Inst. of Comp. Sc., University of
Podlasie, ul. Sienkiewicza 51, 08-110 Siedlce, Poland
Abstract: 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.
Keywords: Promela, Spin, Timed Automata, timed systems, model checking
