|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Océ-Technologies B.V. and Eindhoven University of Technology (THE NETHERLANDS)
|
|---|---|
| Method: |
muCRL
|
| Tools used: |
muCRL toolset
CADP (Construction and Analysis of Distributed Processes) |
| Domain: |
Embedded Systems.
|
| Period: |
2006
|
| Size: |
37 muCRL processes
358153 states and 1101648 transitions |
| Description: |
The R&D department of Océ-Technologies B.V. develops various
professional document systems, ranging from cut sheet to wide format
and from black-and-white to full color systems. The functioning of
these systems is governed by embedded software, responsible for
controlling the hardware and providing functionalities to the user.
The embedded software, which is typically a distributed system, is
subject to increasingly higher requirements on efficiency and quality,
for which formal methods and verification are helpful.
This case-study addresses the formal modelling and verification of the embedded software controlling an automatic document feeder (ADF) system that is part of a copier machine. The ADF automatically moves sheets of paper from its input tray to the scanner of the copier, one at a time, and places every sheet into an output tray once it has been scanned. The ADF consists of various hardware components: pinches, a shoe pressure, sensors, clutches, motors, belts, and trays. Motors can run at constant speed and in one direction, or at various speeds and in both directions; motors of the latter type are equipped with an encoder, which monitors the distance covered so far by the motor, and a controller, which is able to execute profiles specifying sequences of commands to start/stop accelerating/decelerating at a given rate. Three instances of the controlling software run in parallel, each one being in charge of guiding one sheet through the ADF. The instances communicate by global shared variables and synchronize by means of semaphores. The behaviour of each instance is described by an execution sheet, which is a table of state-trigger-response combinations. The behaviour of the ADF system (consisting of shared variables, semaphores, and three instances of the controlling software) was modeled in muCRL. The corresponding state space was generated using the muCRL tools. Then, four different correctness requirements (three safety and one liveness) were identified and specified in modal mu-calculus. After verifying the requirements on the state space using the EVALUATOR model checker of CADP, two errors were discovered in the controlling software of the ADF: a sheet can get stuck in the middle of the copier machine while all motors are idle, and a sheet on its way to the glass plate may be stretched in opposite directions. Solutions to these problems, consisting in adding two new semaphores, are proposed and shown to be correct by checking the requirements successfully on the updated specification of the system. |
| Conclusions: |
This case-study illustrates the usefulness of formal verification for
the analysis of controlling software embedded in real industrial
systems. The behaviour of the ADF system is complex and a significant
amount of work was necessary to understand it precisely starting from
the execution sheets of the software instances. This effort was
rewarded by the ability of using formal verification tools on the ADF
specification, which could be easily checked on a contemporary
desktop computer.
|
| Publications: |
[Ploeger-Somers-07]
B. Ploeger and L. Somers.
"Analysis and Verification of an Automatic Document Feeder".
In Proceedings of the 21st ACM Symposium on Applied Computing SAC
2007 (Seoul, Korea), pp. 1499-1506, ACM, March 2007.
Full version availalable on-line at: http://alexandria.tue.nl/extra1/wskrap/publichtml/200625.pdf or from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Ir. S.C.W. Ploeger Eindhoven University of Technology Department of Mathematics and Computer Science P.O. Box 513 5600 MB Eindhoven The Netherlands Office: HG 6.81 Tel: +31 40 247 2952 Fax: +31 40 246 8508 E-mail: S.C.W.Ploeger@tue.nl |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page