Automatic Document Feeder
An Automatic Document Feeder (ADF) is an important component of a copier
machine. Its task is to feed a document to the scanner automatically, one sheet
at a time. We have analyzed the embedded software of an ADF prototype. We
constructed a model of the ADF in µCRL and expressed seven requirements in
the modal µ-calculus. Next, we used the µCRL and CADP toolsets to check
whether the system meets its requirements. This analysis revealed two errors in
the ADF and we proposed solutions to these problems. We showed that the system
that incorporates these solutions, meets all of the requirements. Also, we
showed that some requirements were too strict. We presented slightly weaker
versions of these requirements and showed that these do hold. In this sense, in
addition to finding errors in the ADF, our analysis also led to a better
understanding of the behaviour the system.
- Type of verification
- Six safety properties and one liveness property were checked on the state
space. Four violations of properties were found, of which two indicated errors
in the system.
- Data size
- The original specification resulted in a state space of around 358.000 states.
The specification that incorporates the solutions to the errors found during
verification, has a state space of around 79.000 states.
- Equipment (computers, CPU, RAM)
- The state space was generated in about 2 minutes on a Pentium 4, 3 GHz machine
with 1 GB of RAM. Model checking of the properties was done on the same
- The model is available as an appendix to [PS06].
- Organizational context
|Contact person:||Bas Ploeger, Technische Universiteit Eindhoven, The
|Other people involved:|
| ||Lou Somers, Technische Universiteit Eindhoven, The
|Institution:||Technische Universiteit Eindhoven, The Netherlands.
| ||Océ Technologies B.V., Venlo, The Netherlands
|Time period:||May 2005 – August 2005
|[PS06]||Bas Ploeger and Lou Somers. Analysis and Verification of an Automatic Document Feeder.
CS-Report 06-25, Technische Universiteit Eindhoven (2006).
|[PS07]||Bas Ploeger and Lou Somers. Analysis and Verification of an Automatic Document Feeder.
In: “Proceedings of the 2007 ACM Symposium on Applied Computing (ACMSAC‘07)”, pages 1499-1505, Seoul, Korea. ACM, March 2007.
Another description of this showcase is available on the CADP homepage.