Midlet Navigation Graphs in JML

11 years 10 months ago
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.
Wojciech Mostowski, Erik Poll
Added 21 May 2011
Updated 21 May 2011
Type Journal
Year 2010
Where SBMF
Authors Wojciech Mostowski, Erik Poll
Comments (0)