A Formal Model of Resource Sharing Conflicts in Multi-Threaded Java

We present a tool for analyzing resource sharing conflicts in multi-threaded Java programs. We model execution of Java programs on a single processor. A Java program is translated into a system of timed automata which is verified by the model checker Uppaal. We also present our ongoing work on formalization of Java semantics and the semantics of timed automata and partial verification of the translation procedure.
 

Online Copy

Report: PDF