Presentation: Midlet Navigation Graphs in JML
When: June 29, 2011, 13:30-14:30
Where: Zi 5126
Who: Wojciech 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.