Midlet Navigation Graphs in JML
In the context of the EU project Mobius on Proof Carrying Code for Java programs (midlets) on mobile devices, the authors 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. Their work was guided by a realistically sized case study developed as demonstrator in the project. They 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.