  Trace analysis can be a useful way to discover problems in a program under
test. Rather than writing a special purpose trace analysis tool, this paper
proposes that traces can usefully be analysed by checking them against a formal
model using a standard model-checker or else an animator for executable
specifications. These techniques are illustrated using a Travel Agent case
study implemented in J2EE. We added trace beans to this code that write trace
information to a database. The traces are then extracted and converted into a
form suitable for analysis by Spin, a popular model-checker, and Pro-B, a
model-checker and animator for the B notation. This illustrates the technique,
and also the fact that such a system can have a variety of models, in different
notations, that capture different features. These experiments have demonstrated
that model-based trace-checking is feasible. Future work is focussed on scaling
up the approach to larger systems by increasing the level of automation.
