Database of Case Studies Achieved Using CADP

Automatic Document Feeder

Organisation: Océ-Technologies B.V. and Eindhoven University of Technology (THE NETHERLANDS)

Method: muCRL

Tools used: muCRL toolset
CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded Systems.

Period: 2006

Size: 37 muCRL processes
358153 states and 1101648 transitions

Description: The R&D department of Océ-Technologies B.V. develops various professional document systems, ranging from cut sheet to wide format and from black-and-white to full color systems. The functioning of these systems is governed by embedded software, responsible for controlling the hardware and providing functionalities to the user. The embedded software, which is typically a distributed system, is subject to increasingly higher requirements on efficiency and quality, for which formal methods and verification are helpful.

This case-study addresses the formal modelling and verification of the embedded software controlling an automatic document feeder (ADF) system that is part of a copier machine. The ADF automatically moves sheets of paper from its input tray to the scanner of the copier, one at a time, and places every sheet into an output tray once it has been scanned. The ADF consists of various hardware components: pinches, a shoe pressure, sensors, clutches, motors, belts, and trays. Motors can run at constant speed and in one direction, or at various speeds and in both directions; motors of the latter type are equipped with an encoder, which monitors the distance covered so far by the motor, and a controller, which is able to execute profiles specifying sequences of commands to start/stop accelerating/decelerating at a given rate. Three instances of the controlling software run in parallel, each one being in charge of guiding one sheet through the ADF. The instances communicate by global shared variables and synchronize by means of semaphores. The behaviour of each instance is described by an execution sheet, which is a table of state-trigger-response combinations.

The behaviour of the ADF system (consisting of shared variables, semaphores, and three instances of the controlling software) was modeled in muCRL. The corresponding state space was generated using the muCRL tools. Then, four different correctness requirements (three safety and one liveness) were identified and specified in modal mu-calculus. After verifying the requirements on the state space using the EVALUATOR model checker of CADP, two errors were discovered in the controlling software of the ADF: a sheet can get stuck in the middle of the copier machine while all motors are idle, and a sheet on its way to the glass plate may be stretched in opposite directions. Solutions to these problems, consisting in adding two new semaphores, are proposed and shown to be correct by checking the requirements successfully on the updated specification of the system.

Conclusions: This case-study illustrates the usefulness of formal verification for the analysis of controlling software embedded in real industrial systems. The behaviour of the ADF system is complex and a significant amount of work was necessary to understand it precisely starting from the execution sheets of the software instances. This effort was rewarded by the ability of using formal verification tools on the ADF specification, which could be easily checked on a contemporary desktop computer.

Publications: [Ploeger-Somers-07] B. Ploeger and L. Somers. "Analysis and Verification of an Automatic Document Feeder". In Proceedings of the 21st ACM Symposium on Applied Computing SAC 2007 (Seoul, Korea), pp. 1499-1506, ACM, March 2007.
Full version availalable on-line at: http://alexandria.tue.nl/extra1/wskrap/publichtml/200625.pdf
or from the CADP Web site in PDF or PostScript
Contact:
Ir. S.C.W. Ploeger
Eindhoven University of Technology
Department of Mathematics and Computer Science
P.O. Box 513
5600 MB Eindhoven
The Netherlands
Office: HG 6.81
Tel: +31 40 247 2952
Fax: +31 40 246 8508
E-mail: [email protected]
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Thu Feb 11 12:22:03 2021.

Back to the CADP case studies page