Affiliations: IT&ACS, Polish Academy of Sciences, ul. Bałtycka
5, 44-100 Gliwice, Poland. [email protected] | IM&CS, Jan Długosz University, Al. Armii Krajowej
13/15, 42-200 Cz�stochowa, Poland. [email protected];
[email protected]
Note: [] Address for correspondence: IM&CS;, Jan Długosz University,
Al. Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland
Abstract: The model checking tools Uppaal and VerICS accept a description of a
network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify
a concurrent programwritten in Java by means of these tools, first a TADD model
of the program must be build. Therefore, we have developed the J2TADD tool that
translates a Java program to a network of TADDs; the paper presents this tool.
The J2TADD tool works in two stages. The first one consists in
translation of a Java code to an internal assembly language (IAL). Then, the
resulting assembly code is translated to a network of TADDs. We exemplify the
use of the translator by means of the following well-known concurrency examples
written in Java: race condition problem, dining philosophers problem, single
sleeping barber problem and readers and writers problem.
