Information Technology Reference
In-Depth Information
transitions between the screens caused by user actions, i.e.
Commands
. Finally,
in [5] the arrows (transitions) also have interpretations, as they indicate which
sensitive operations that may be performed during a given transition.
Send [SMS]
Main
End
start
Fig. 5.
Statechart diagram: a simple midlet navigation graph
Such a notion of a graph can also be easily represented by a UML state chart
diagram. The states of the diagram represent application screens, the arrows
represent user commands, and arrow guards can be used to mark sensitive op-
erations. A very simple example is given in Fig. 5. In this example, from the
main screen a user can choose the
Send
command, in which case at most one
SMS would possibly be sent over the network, or press
End
,inwhichcasethe
application will simply terminate. Furthermore, using the UML state stereotypes
we can indicate additional properties of screens, e.g. whether an alert screen is
displayed only for a given period of time indicated by the timeout parameter
(and hence performing a transition to another screen without user interaction).
This last aspect is not covered in [5].
4 Navigation Graphs in JML
This section gives the semantics of a navigation graph in terms of JML. In other
words, we define a mapping from navigation graphs to JML annotations. Our
effort is divided into two parts. We start with the first part, which is to specify,
in a generic way, the midlet API calls. The API specifications can then be used
when specifying a particular midlet behaviour to reflect a given midlet navigation
graph in the second part that we discuss later.
4.1 Relevant API Methods
We want our JML specifications to be easy to verify for the verification tools.
Hence we only specified those aspects that are needed for navigation graphs, and
we avoided constructs that are challenging for verification, as discussed later. Our
specifications often use so-called ghost variables [4], which are specification-only
variables, to model relevant aspects of the state of the platform (incl. the GUI).
As mentioned before, two aspects of the API need to be specified: the GUI
and security-sensitive operations. For the GUI, we need to specify the
Display
class, where a ghost field
current
tracks what is being displayed:
Search WWH ::
Custom Search