Modelling Java concurrency: An approach and a UPPAAL library

To effectively cope with correctness issues of concurrent and timed systems, the use of formal tools is mandatory. This paper proposes an original approach to modeling and exhaustive verification of Java-based concurrent systems which relies on the popular UPPAAL model checker. More precisely, a library of UPPAAL timed automata (TA) reproducing the semantics of major Java concurrent and synchronization mechanisms was developed, which fosters a smooth transition from specification down to implementation. The library includes such common control structures like semaphores and monitors, both classic and Java specific. The paper describes the developed TA library and shows its practical use by means of examples. Finally, an indication of on-going and future work directions is drawn in the conclusion.