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.
|Contact person:||Bas Ploeger, Technische Universiteit Eindhoven, The Netherlands.|
|Other people involved:|
|Lou Somers, Technische Universiteit Eindhoven, The Netherlands.|
|Institution:||Technische Universiteit Eindhoven, The Netherlands.|
|Océ Technologies B.V., Venlo, The Netherlands|
|Time period:||May 2005 – August 2005|