Analysis and verification of an automatic document feeder

B. Ploeger, L.J.A.M. Somers

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)
    1 Downloads (Pure)


    Modern copying machines are versatile and complex systems in which embedded software plays an essential role. The progress towards faster and more stable machines that can satisfy ever growing customers' needs, places strict requirements on the efficiency and quality of such software. In order to meet these requirements, the software should be well-designed and free of errors. Using modern formal verification techniques, software designs can be checked for errors and deadlocks so that their quality can be assessed and improved at an early stage of the development process. In this paper, we analyze the embedded software of an Automatic Document Feeder (ADF). ADFs are important components of copier machines. The ADF studied here is a prototype developed by Océ-Technologies B.V., a company that develops professional printing systems. We construct a model of the ADF in µcrl, a process algebra-based specification language, and express the system's requirements in the modal µ-calculus. Next, we use the µcrl and Cadp tool sets to check whether the system meets its requirements. This analysis reveals important errors in the ADF and we propose solutions to these problems. Also, we show that some requirements that engineers assumed to be valid, are too strict. We present slightly weaker versions of these requirements and show 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.
    Original languageEnglish
    Title of host publicationProceedings of the 22nd Annual ACM Symposium on Applied Computing (SAC 2007) 11-15 March 2007 Seoul, Korea
    EditorsY. Cho, R.L. Wainwright, H. Haddad, S.Y. Shin, Y.W. Koo
    Place of PublicationNew York, USA
    PublisherAssociation for Computing Machinery, Inc
    ISBN (Print)1-59593-480-4
    Publication statusPublished - 2007
    Event22nd ACM Symposium on Applied Computing (SAC 2007) - COEX Convention Center, Seoul, Korea, Republic of
    Duration: 11 Mar 200715 Mar 2007
    Conference number: 22


    Conference22nd ACM Symposium on Applied Computing (SAC 2007)
    Abbreviated titleSAC 2007
    Country/TerritoryKorea, Republic of
    Internet address


    Dive into the research topics of 'Analysis and verification of an automatic document feeder'. Together they form a unique fingerprint.

    Cite this