Midlet Navigation Graphs in JML

Abstract. 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.

• Type: Journal
• Year: 2010
• Where: SBMF
• Authors: Wojciech Mostowski, Erik Poll
• Keywords: Formal Methods, JML Specifications, Midlet Navigation Graphs, Navigation Graphs, SBMF 2010