June 29, 2011Presentation: Midlet Navigation Graphs in JML
Room: Zi 5126Wojciech Mostowski

In the context of the EU project Mobius on Proof Carrying Code for Java
programs (midlets) on mobile devices, we present a way to express midlet
navigation graphs in JML.  Such navigation graphs express certain
security policies for a midlet. The resulting JML specifications can be
automatically checked with the static checker ESC/Java2. Our work was
guided by a realistically sized case study developed as demonstrator in
the project.  We discuss practical difficulties with creating efficient
and meaningful JML specifications for automatic verification with a
lightweight verification tool such as ESC/Java2, and the potential use
of these specifications for PCC.