Specification and Verification of Concurrent Behaviour in Android Applications

title:Specification and Verification of Concurrent Behaviour in Android Applications
keywords:Android, formal specification, formal verification, JML
topics:Languages, Logics and semantics
contact:prof.dr. M. Huisman
to be started:any time


The Android Operating System is based almost entirely on Java, however, the general characteristics of a typical Android application is somewhat different from well-known desktop applications. In particular, concurrency is inherently at the base of each Android application - applications are GUI based and controlled exclusively through events. Furthermore, the Android hides many aspects of concurrency under the hood of the system API - a higher level framework for concurrency is provided through message handlers, looper threads, etc. [6]. This project is about developing formal techniques tailored for the specification and verification of Android applications with respect to all kinds of such concurrent behaviours. The generally established specification languages and verification techniques were in principle designed for (Java) programs that are mostly sequential. They were successfully applied to previous (simpler) Java mobile platforms, like Java Card for programming smart cards [1], or Java2ME for mobile devices [2]. The existing concurrency extensions to verification techniques [7,9,10] deal mostly with explicit concurrency, like direct thread creation and execution, or concurrent access to shared data. For this project, all aspects of implicit and hidden concurrency, as well as the extended concurrency API [4,5] of Android shall be studied and new specification and verification techniques should be proposed to support formal verification of Android applications. This would possibly include extensions of the specification language, extensions of the verification logic, and methods for automatically generating specifications.

The specification language that this project should concentrate on is the Java Modeling Language (JML) [3], a de-facto standard formal specification language for Java. The two possible verification techniques to be investigated in the project are the Permission-Based Separation Logic as implemented in the VerCors tool [7], or the Java Dynamic Logic as implemented in KeY interactive verifier for Java [1,8].

Literature and Links

  1. 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).
  2. W. Mostowski and E. Poll. Midlet Navigation Graphs in JML. Post Proceedings, 13th Brazilian Symposium on Formal Methods (SBMF 2010).
  3. The Java Modeling Language (JML) Home Page: http://www.jmlspecs.org/
  4. Masoumeh Al. Haghighi Mobarhan. Formal Specification of Selected Android Core Applications and Library Functions. Master thesis, Chalmers University of Technology, Sweden, 2011.
  5. Afshin Amighi, Stefan Blom, Marieke Huisman, Wojciech Mostowski, and Marina Zaharieva-Stojanovski. Formal Specifications for Java's Synchronisation Classes. Proceedings, 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, February 2014, pages 725-733, © IEEE Computer Society.
  6. The Android API Reference, http://developer.android.com/reference/packages.html
  7. Afshin Amighi, Stefan Blom, Saeed Darabi, Marieke Huisman, Wojciech Mostowski, Marina Zaharieva-Stojanovski, Verification of Concurrent Systems with VerCors. 14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models, LNCS 8483, Springer 2014.
  8. Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich, The KeY Platform for Verification and Analysis of Java Programs. To appear in 6th Working Conference on Verified Software: Theories, Tools and Experiments, Springer 2014.
  9. K. Rustan M. Leino, Peter Müller, and Jan Smans, Verification of concurrent programs with Chalice, in Lecture notes of FOSAD, LNCS 5705, Springer 2009.
  10. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens, VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods, LNCS 6617, Springer 2011.