Midlet Navigation Graphs in JML - Formal Methods: Foundations and Applications - page 30

The translation of a midlet navigation graph to JML, which we did by hand,
could be automated, as done for state diagrams by the AutoJML tool [9]. An
alternative to coding up the midlet navigation graph in JML pre- and postcon-
ditions, as we have done, would be to use special specification constructs for
temporal properties [21] or CSP-style contraints on method sequences [16].
Our approach has been shown to work on a non-trivial (albeit still very small)
midlet, the Mobius Quiz game demonstrator, which consists of 13 classes and
1350 lines of code, which was then verified using ESC/Java2. Once the midlet
navigation graph is expressed by JML annotations, further annotations of the
midlet are needed for the verification to go through, e.g. to rule out Null-
PointerExceptions , etc. This further annotation took an effort in the order of
days.
As explained in Sect. 4.2, a technical complication is any use of dynamically
created Displayable objects in midlet code, as additional static (ghost) fields
have to be introduced to refer to these objects in specifications.
As discussed in Sect. 5, the main complication is the semantics of (ob-
ject) invariants. JML's visible state semantics, which ESC/Java2 tries to check
(ESC/Java2 is not guaranteed to be sound in this respect), is often stronger than
we really need or want. The need for more flexible ways for dealing with invari-
ants is of course widely recognised. Spec# [1] provides one such an approach,
and alternatives are systematically compared in [6].
It is very important that the API specifications used are not too rich (i.e.
too expressive) and only specify the aspects relevant for the navigation graphs.
Otherwise the job of annotating and verifying the midlet can become much more
complicated. Also, as discussed in Sect. 5, Singleton classes occur often in the
MIDP API and in typical midlets. Specifying this in JML is a bit clumsy, and
(hence) verification with ESC/Java2 seems more complicated than it needs to
be. Better ways of dealing with this (possibly by additional primitives in JML)
could simplify matters substantially.
A major caveat in our work is that we ignore concurrency. However, the con-
currency patterns used in midlets are very simple - essentially, implementations
of commandAction sometimes start up a worker thread to hand back control to
the GUI as soon as possible - so might well be verifiable using a simple approach.
Midlet navigation graphs express safety properties of code, constraining the
possible behaviour. This means that crashing of a midlet, say with a Null-
PointerException , can never violate the policy expressed by a navigation graph.
This might allow verification to be simplified further: if we can guarantee that
code never catches say NullPointerException s - which could be checked using
a simple static analysis - then in the verification we could safely ignore the
possibility of NullPointerException s. This is supported by some verification
tools, e.g. the KeY tool [3] offers an option for such simplified reasoning.
PCC. The overall goal of the EU project Mobius, in which this research was
carried out, was to provide a Proof-Carrying Code (PCC) framework for Java on
mobile devices [2]. PCC [17] involves (i) some security policy, (ii) some untrusted
code, and (iii) a proof that this code obeys the policy that can be checked.