Abstract

This thesis describes the automatic verification and analysis of a printer of Océ by means of test results in the form of logfiles.

Océ is a company that develops high performance, state-of-the-art printers that produce up to 250 pages per minute. To test the complex software within these printers, all printer processes write their actions into a global logfile. When executing tests, an automatic analysis and verification of logfiles is useful, especially when these tests are automated and performed on printers under development. Currently, these logfiles are often inspected manually, which is a cumbersome and time-consuming task.

For automatic verification and analysis the logfile is transformed to a log model, which only contains log statements of functionality for tests relevant. The same (relevant) functionality is modeled in a specification. This specification consist of a composition of reference, synchronization and test-specific models representing protocols, relations between protocols, and behaviour adjusted to tests. It is defined in the formal language LOTOS. The relation between the log model and the specification is a trace membership relation, which means that a log model, if it represents correct printer behaviour, is a member of the traces formed by the specification.

This relation is implemented in a tool chain, consisting of a preprocessor, an editor, two compilers, and a Testlog verifier. The preprocessor transforms the logfile into a log model. LOTOS compilers compile the LOTOS specification, which is made in the LOTOS editor, into C code, and the Testlog verifier checks whether a relation between the log model and the compiled specification exists. Depending on the printer behaviour a verdict, true or false, is returned. In the latter case, a sequence of transitions is given which leads to the first unexpected transition in the log model.

With this tool chain, three protocols with connecting relations were analyzed with logfiles from 15.000 to 700.000 lines. All known errors where identified correctly and in almost all cases the verification times where short (less than 16 minutes). In some cases, with many protocol instances in parallel, they exceeded one hour.

Additional Resources

1. The paper