AVATR Tool for Analyzing Test Results of Océ Printers

Organisation:	University of Twente (THE NETHERLANDS)
Functionality:	Automatic verification and analysis of test results.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2009
Description:	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.
Conclusions:	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.
Publications:	[Rietema-09] Richard Rietema. "Automatic Verification and Analysis of Test Results of Océ Printers". MSc thesis, University of Twente, The Netherlands, May 2009. Available on-line at: http://fmt.cs.utwente.nl/msc-completed/rietema-msc-thesis.pdf or from the CADP Web site in PDF or PostScript
Contact:	Mariëlle Stoelinga Dept. of Computer Science Formal Methods & Tools P.O. Box 217 7500 AE Enschede The Netherlands Tel: +31 53 489 3773 Fax: +31 53 489 3247 Email: marielle@cs.utwente.nl
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page