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. © 2011 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Mostowski, W., & Poll, E. (2011). Midlet navigation graphs in JML. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6527 LNCS, pp. 17–32). https://doi.org/10.1007/978-3-642-19829-8_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
