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

graph from bytecode. In this paper we present a way to express the semantics
of navigation graphs in terms of a specification at source code level. The formal
specification language we use for this is Java Modelling Language (JML) [14].
Our work was guided by one of the Mobius case studies, a quiz game mi-
dlet developed by industrial partner TLS 2 [15]. This is the biggest case study of
the project and it exhibited some problems during the JML annotation pro-
cess and also during verification with the extended static checker for Java,
ESC/Java2 [11]. We will discuss the problems we encountered with developing
the JML specification and verifying it in detail.
The rest of this paper is organised as follows. Sect. 2 gives an introduction
to the MIDP application structure. Sect. 3 describes midlet navigation graphs
in more detail. Sect. 4 discusses the translation of the midlet navigation graphs
in JML based on the Mobius case study. Finally, Sect. 6 summarises our results
and discusses the potential for PCC.
2 MIDP Infrastructure
The notion of midlet navigation graphs relies on the infrastructure of the Java2
Micro Edition platform (J2ME) 3 for small devices, such as mobile phones or
PDAs. The main building blocks of the J2ME platform of interest are the Mo-
bile Information Device Profile (MIDP) Java API and the Connected Limited
Device Configuration (CLDC) Java API. The former API deals with output to
the display and input from the user via the keypad of the device. The latter
API is mostly responsible for device's communication with the outside world.
J2ME is often referred to as MIDP, and CLDC is usually assumed to be part
of J2ME/MIDP when mobile phones or PDAs are considered. The applications
that run on these devices are called midlets.
GUI. A navigation graph is related to the phone's display and sensitive opera-
tions that a midlet can possibly perform. In the following we discuss the relevant
parts of the MIDP API. As a presentation aid we use UML.
Every midlet, represented by the MIDlet class, has a unique associated Disp-
lay object, which manages the display and the input devices. The static method
Display.getDisplay(MIDlet m) returns the display associated with a midlet.
The various kinds of things that can be displayed on the Display object are
instances of the subclasses of Displayable , shown in Fig. 1. Invoking the meth-
od void setCurrent(Displayable nextDisplayable) on a Display changes
what it displays, possibly after a short delay. A List presents a list of choices, i.e.
a menu, that the user can scroll through and select. A TextBox allows the user
to enter and edit text. A Form presents an arbitrary mixture of items, which can
for instance be images or (read-only or editable) text fields. Finally, an Alert
is a screen that is shown for a short period of time, either until some time-
out or a key press. Alerts can also be displayed by invoking the method void
2 http://www.tls.pl
3 http://java.sun.com/javame/index.jsp