University of Twente (THE NETHERLANDS)
Automatic verification and analysis of test results.
CADP (Construction and Analysis of Distributed Processes)
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 that is relevant for testing. The same (relevant) functionality is modeled as a LOTOS specification consisting of a composition of reference, synchronization, and test-specific models representing protocols, relations between protocols, and behaviours adjusted to tests. 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 the AVATR tool chain, consisting of a preprocessor, a LOTOS editor, two compilers, and a Testlog verifier. The preprocessor transforms the logfile into a log model. The LOTOS specification, developed using the LOTOS editor, is compiled into C code using the CAESAR and CAESAR.ADT compilers of the CADP toolbox. The Testlog verifier, based on the EXHIBITOR tool of CADP, 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.
Using the AVATR 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 less than 16 minutes. In some cases, with many protocol instances in parallel, they exceeded one hour.
The AVATR tool chain is capable of automatic verification and analysis
of test results of printers built by Océ. The feasibility study
shows acceptable running times, even for many protocol instances.
Using AVATR, logfiles can be verified and analyzed more thoroughly
than with existing methods.
"Automatic Verification and Analysis of Test Results of Océ
Printers". MSc thesis, University of Twente, The Netherlands,
Available on-line at: http://fmt.cs.utwente.nl/msc-completed/rietema-msc-thesis.pdf
or from our FTP site in PDF or PostScript
Dept. of Computer Science
Formal Methods & Tools
P.O. Box 217
7500 AE Enschede
Tel: +31 53 489 3773
Fax: +31 53 489 3247
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|