Analysis and verification of an automatic document feeder

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

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    3 Citaten (Scopus)
    1 Downloads (Pure)

    Samenvatting

    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.
    Originele taal-2Engels
    TitelProceedings of the 22nd Annual ACM Symposium on Applied Computing (SAC 2007) 11-15 March 2007 Seoul, Korea
    RedacteurenY. Cho, R.L. Wainwright, H. Haddad, S.Y. Shin, Y.W. Koo
    Plaats van productieNew York, USA
    UitgeverijAssociation for Computing Machinery, Inc
    Pagina's1499-1505
    ISBN van geprinte versie1-59593-480-4
    StatusGepubliceerd - 2007
    Evenement22nd ACM Symposium on Applied Computing (SAC 2007) - COEX Convention Center, Seoul, Zuid-Korea
    Duur: 11 mrt. 200715 mrt. 2007
    Congresnummer: 22
    http://www.sigapp.org/sac/sac2007/

    Congres

    Congres22nd ACM Symposium on Applied Computing (SAC 2007)
    Verkorte titelSAC 2007
    Land/RegioZuid-Korea
    StadSeoul
    Periode11/03/0715/03/07
    AnderSAC 2007, Seoul, Korea
    Internet adres

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Analysis and verification of an automatic document feeder'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit