IOS Press A translator of Java programs to TADDs

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 program written 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. 1