Back to University of Twente portal
| author: | Alexander Drechsel |
| title: | Java Modeling Language Extensions for Android Applications |
| keywords: | JML, Android, formal specification, formal verification |
| topics: | Languages |
| committee: |
Wojciech Mostowski
, Marieke Huisman |
| end: | June 2014 |
Description
The Java Modeling Language (JML) is a formal specification language designed especially for Java. The use of JML enables several levels of supporting program correctness. It starts with simply formally documenting the code, then run-time assertion checking can be used on the JML annotated code to discover run-time bugs, and finally Java programs can be fully verified to be correct with respect to JML specifications using various automated or interactive program verifiers.
JML was initially designed with regular desktop Java applications in mind, however, it has been also successfully used with very specific Java platforms, like Java Card for programming smart cards, or Java2ME for mobile devices, see for example [1,2]. The new big Java player now is the Android operating system that is in principle fully Java based. The general characteristics of a typical Android application is somewhat different from the desktop application. First of all, Android applications have multiple entry points, that is, applications are controlled through events only and the the well know main method (or its counter part) is hidden in the Android OS. Then, the Android GUIs are very specific, stored and generated from special resource files. Finally, due to the specifics of the Android devices, each application is required to secure a number of necessary access rights to be able to fully use the OS API.
The goal of this project is to identify and develop possible JML extensions for the purpose of specifying and verifying Android applications. As part of the project small specification case studies should be developed.
Literature and Links
- W. Mostowski. A Case Study in Formal Verification using Multiple Explicit Heaps. Proceedings, 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS).
- W. Mostowski and E. Poll. Midlet Navigation Graphs in JML. Post Proceedings, 13th Brazilian Symposium on Formal Methods (SBMF 2010).
- OpenJML: http://openjml.org/
- Masoumeh Al. Haghighi Mobarhan. Formal Specification of Selected Android Core Applications and Library Functions. Master thesis, Chalmers University of Technology, Sweden, 2011.