Portal de Periódicos da CAPES

Midlet Navigation Graphs in JML

2011; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-19829-8_2

1611-3349

Wojciech Mostowski, Erik Poll,

Formal Methods in Verification

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.