Information Technology Reference
In-Depth Information
3 Empirical Results
Once a number of game properties were formalized as LTL-FO
+
formulæ, we
devised an experimental setup to assess the performance of our runtime monitor-
ing approach in actual runs of the game.
2
As we have seen, any errors caught by
a monitor should be identified before the next frame, yielding an upper bound
of 17 to 33 ms for the processing of each batch of events. Any processing time
slower than this would either slow down the game and cause jerky animation, or
have the monitor increasingly lag on the current game state and fill some event
buffer.
The BeepBeep runtime monitor
3
[3] was selected to be inserted into the game,
since it was developed in Java and uses LTL-FO
+
formulæ as its input language.
The BeepBeep monitor accepts events in the form of XML strings. Some strings
are constant, while others like this one are dynamically created based on the
specific parameters of the event (enemy IDs, etc.). For example, the following
shows the instrumentation to generate an event indicating that some enemy died:
MonitorTimer.Instance().updateWatchers("
<action>
<name>
EnemyDead
</name>
<id>
"+id+"
</id>
</action>
");
The game's code was manually instrumented to produce these events; about 30
locations in the code had instruction of this kind inserted. We could have chosen
AspectJ [6] to facilitate the instrumentation but we decided not to because this
solution is Java-specific, and most games use languages like C++ or even unique
ones like UnrealScript. Relying on AspectJ would not faithfully represent the
restrictions one shall face when monitoring video games in general.
To keep track of the different outcomes for each property, we also added some
elements to the game's GUI. First, circles of colour, each representing a property,
can be found on the lower left part of the screen. A green dot indicates a property
evaluates to true on the sequence of events received so far, while red indicates
it evaluates to false. Since each monitor is constantly queried on a finite trace
prefix, the value of some properties may not be defined yet; this is indicated by a
yellow dot. For debugging purposes, we also print the last two events produced at
the top of the window. The lower-right corner displays in real time the overhead
incurred by the presence of the monitors.
Finally, in order to make sure that our monitor can actually intercept game-
play bugs, we manually performed modifications to the game's code to create
2
The instrumented version of Inifinite Mario and the runtime monitor can be down-
loaded from
http://github.com/sylvainhalle/BeepKitu
