A Translator of Java Programs to TADDs | Zendy

Artur Rataj | Zendy; Bożena Woźna-Szcześniak | Zendy; Andrzej Zbrzezny | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Translator of Java Programs to TADDs

Author(s) -

Artur Rataj,

Bożena Woźna-Szcześniak,

Andrzej Zbrzezny

Publication year - 2009

Publication title -

fundamenta informaticae

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.311

H-Index - 67

eISSN - 1875-8681

pISSN - 0169-2968

DOI - 10.3233/fi-2009-0104

Subject(s) - computer science , java , programming language , generics in java , concurrency , java concurrency , real time java , java annotation , java modeling language , strictfp , code (set theory) , automaton , theoretical computer science , set (abstract data type)

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research