
Model-Based GUI Testing of Smartphone Applications: Case S60
TM
and Linux
r
535
Startup-rm
end_awExitMessaging
start_awExitMessaging
end_awStartMessaging
start_awStartMessaging
kw_PressHardKey <SoftRight>
FIGURE 18.5
The refinement machine for the Messaging Startup model. The implementation for the
awStartMessaging action is empty since the generated task switcher launches applica-
tions automatically as needed. The action can still be used in coverage requirements and
debugging.
ALLOW<@PARENT: ToMessagesExist>
ALLOW<@PARENT: ToMessagesMayExist>
ALLOW<@PARENT:
MessagesMayExist>
ALLOW<@PARENT: ToMessagesExist>
ALLOW<@PARENT:
MessagesExist>
ALLOW<@PARENT:
NoMessagesExist> ...