Abstraction and Verification of Properties of a Real-Time Java

We present a tool for analysing resource sharing conflicts in multithreaded Java programs. Java programs are translated to timed automata models verified afterwards by the Uppaal model checker. Analysed programs are annotated with timing information indicating the execution duration of a particular statement. Based on the timing information, the analysis of execution paths is performed, which gives an answer whether resource sharing conflicts are possible in a multithreaded Java program. If the analysis succeeds, resource locks may be eliminated from the Java program.
 

Online Copy

Conference version: PDF

BibTeX Entry

@incollection{baklanova12:_abstr_verif_proper_real_time_java,
  author =       {Baklanova, Nadezhda and Strecker, Martin},
  title =        {Abstraction and Verification of Properties of a Real-Time
                  Java},
  booktitle =    {ICT in Education, Research, and Industrial Applications},
  year =         {2013},
  isbn =         {978-3-642-35736-7},
  volume =       {347},
  series =       {Communications in Computer and Information Science},
  editor =       {Ermolayev, Vadim and Mayr, Heinrich C. and Nikitchenko,
                  Mykola and Spivakovsky, Aleksander and Zholtkevych,
                  Grygoriy},
  doi =          {10.1007/978-3-642-35737-4_1},
  url =
                  {http://www.irit.fr/~Martin.Strecker/Publications/icteri2012.html},
  publisher =    {Springer Berlin Heidelberg},
  keywords =     {timed automaton; Java; multithreading; deadlock; resource
                  sharing conflict; Uppaal},
  pages =        {1-18}
}