Article

Analysis and verification of an automatic document feeder

Authors:

Lou SomersAuthors Info & Claims

SAC '07: Proceedings of the 2007 ACM symposium on Applied computing

Pages 1499 - 1505

https://doi.org/10.1145/1244002.1244324

Published: 11 March 2007 Publication History

Abstract

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.

References

[1]

Rajeev Alur, Thao Dang, Joel M. Esposito, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, and Oleg Sokolsky. Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE, 91(1):11--28, 2003.

[2]

J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1990.

Digital Library

[3]

G. Behrmann, A. David, and K. G. Larsen. A tutorial on uppaal. In M. Bernardo and F. Corradini, editors, Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, LNCS 3185, pages 200--236. Springer-Verlag, September 2004.

[4]

S. Blom, W. Fokkink, J. F. Groote, I. van Langevelde, B. Lisser, and J. van de Pol. μCRL: A toolset for analysing algebraic specifications. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Proceedings of the 13th Conference on Computer-Aided Verification (CAV'01), LNCS 2102, pages 250--254. Springer, July 2001.

Digital Library

[5]

T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1):25--59, January 1987.

Digital Library

[6]

J.-C. Fernandez, H. Garavel, A. Kerbrat, A. Mounier, R. Mateescu, and M. Sighireanu. CADP: a protocol validation and verification toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Verification CAV, LNCS 1102, pages 437--440, New Brunswick, NJ, USA, July/August 1996. Springer Verlag.

Digital Library

[7]

W. J. Fokkink, J. F. Groote, J. Pang, B. Badban, and J. C. van de Pol. Verifying a sliding window protocol in μCRL. In C. Rattray, S. Maharaj, and C. Shankland, editors, Proceedings 10th Conference on Algebraic Methodology and Software Technology - AMAST'04, LNCS 3116, pages 148--163. Springer, July 2004.

[8]

H. Garavel, F. Lang, and R. Mateescu. An overview of CADP 2001. Technical Report RT-0254, INRIA, France, 2001.

[9]

Jan Friso Groote, Jun Pang, and Arno G. Wouters. Analysis of a distributed system for lifting trucks. Journal of Logic and Algebraic Programming, 55(1--2):21--56, 2003.

[10]

J. F. Groote and A. Ponse. The syntax and semantics of μCRL. Report CS-R9076, CWI, Amsterdam, 1990.

[11]

C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

Digital Library

[12]

G. J. Holzmann. The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, 2003.

Digital Library

[13]

Pao-Ann Hsiung, Win-Bin See, Trong-Yen Lee, Jih-Ming Fu, and Sao-Jie Chen. Formal verification of embedded real-time software in component-based application frameworks. In Eighth Asia-Pacific Software Engineering Conference (APSEC), pages 71--78. IEEE Computer Society, 2001.

Digital Library

[14]

D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333--354, 1983.

[15]

Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, and Arne Skou. Testing real-time embedded software using UPPAAL-TRON: an industrial case study. In Wayne Wolf, editor, Proceedings of the 5th ACM International Conference On Embedded Software, pages 299--306, Jersey City, NJ, USA, 2005. ACM.

Digital Library

[16]

Radu Mateescu and Mihaela Sighireanu. Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Science of Computer Programming, 46(3):255--281, March 2003.

Digital Library

[17]

R. Milner. A Calculus of Communicating Systems. LNCS 92. Springer-Verlag, 1980.

Digital Library

[18]

Bas Ploeger and Lou Somers. Analysis and Verification of an Automatic Document Feeder. CS-Report 06--25, Technische Universiteit Eindhoven, 2006.

[19]

J. van de Pol and M. Valero Espada. Verification of JavaSpaces (TM) Parallel Programs. In J. Lilius, F. Balarin, and Machado R. J., editors, Proceedings 3rd International Conference on Application of Concurrency to System Design (ACSD), Guimaraes, Portugal, pages 196--205. IEEE, June 2003.

Digital Library

[20]

J. P. Queille and J. Sifakis. Fairness and related properties in transition systems: a temporal logic to deal with fairness. Acta Informatica, 19(3):195--220, 1983.

Digital Library

[21]

W. Reisig. Petri Nets, An Introduction. Springer-Verlag, Berlin, 1985.

Digital Library

[22]

A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998.

Digital Library

[23]

C. Shankland and M. B. van der Zwaag. The tree identify protocol of IEEE 1394 in μCRL. Formal Aspects of Computing, 10:509--531, 1998.

[24]

Yang Zhang and Alan K. Mackworth. Design and analysis of embedded real-time systems: An elevator case study. Technical Report TR-93-04, Department of Computer Science, University of British Columbia, February 1993.

Digital Library

Cited By

Groote JOsaiweran AWesselius J(2011)Analyzing the effects of formal methods on the development of industrial control softwareProceedings of the 2011 27th IEEE International Conference on Software Maintenance10.1109/ICSM.2011.6081983(467-472)Online publication date: 25-Sep-2011
https://dl.acm.org/doi/10.1109/ICSM.2011.6081983
Friso Groote JMathijssen A"Reniers," MUsenko Yvan Weerdenburg M(2010)Analysis of Distributed Systems with mCRL2Process Algebra for Parallel and Distributed Processing10.1201/9781420064872.pt2Online publication date: 31-Jan-2010
https://doi.org/10.1201/9781420064872.pt2

Index Terms

Analysis and verification of an automatic document feeder

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Automatic Document Summarization using Sentiment Analysis
ICIA-16: Proceedings of the International Conference on Informatics and Analytics

With the advent of information revolution, electronic documents have become the powerhouse of business and academic information. Modern organizations handle terabytes of data in text format alone. In order to fully understand and utilize these documents,...
Parameterised Process Algebraic Verification by Precongruence Reduction
ACSD '09: Proceedings of the 2009 Ninth International Conference on Application of Concurrency to System Design

Decidability of the parameterised verification problem is shown for a class of systems and safety properties given as (multiply) parameterised labelled transition systems with an (infinite) set of valuations representing the allowed parameter values. ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '07: Proceedings of the 2007 ACM symposium on Applied computing

March 2007

1688 pages

ISBN:1595934804

DOI:10.1145/1244002

Conference Chairs:
Yookun Cho
Seoul National University, Seoul, Korea
,
Roger L. Wainwright
University of Tulsa, Tulsa, Oklahoma
,
Hisham M. Haddad
Kennesaw State University, Kennesaw, Georgia
,
Sung Y. Shin
South Dakota State University, Brookings, South Dakota
,
Program Chair:
Yong Wan Koo
The University of Suwon, Gyeongggi-do, Korea

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 March 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SAC07

Sponsor:

SIGAPP

SAC07: The 2007 ACM Symposium on Applied Computing

March 11 - 15, 2007

Seoul, Korea

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
194
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 09 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Groote JOsaiweran AWesselius J(2011)Analyzing the effects of formal methods on the development of industrial control softwareProceedings of the 2011 27th IEEE International Conference on Software Maintenance10.1109/ICSM.2011.6081983(467-472)Online publication date: 25-Sep-2011
https://dl.acm.org/doi/10.1109/ICSM.2011.6081983
Friso Groote JMathijssen A"Reniers," MUsenko Yvan Weerdenburg M(2010)Analysis of Distributed Systems with mCRL2Process Algebra for Parallel and Distributed Processing10.1201/9781420064872.pt2Online publication date: 31-Jan-2010
https://doi.org/10.1201/9781420064872.pt2

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten