Development and Verification of a Collaborative Printing Environment

In this paper, we propose a printing environment utilizing collaboration to offer more reliable printing environment. In the proposed environment, printers are clustered, and collaborative printing is carried out among clusters if one cluster is very busy and others are not. We also work on the formal verification problem of such collaborative environment, since a number of properties must be satisfied in the environment to guarantee the secure and safe printing. To prove such properties, we apply model checking methods to the developed environment. We have developed a simulator of the proposed environment, and show that it can work effectively even if some printers are out of order, or out of paper. Also, applying model checking, we successfully prove the properties that must be satisfied in such printing environments.