An experience in proving regular networks of processes by modular model checking (Q1323369)

This paper presents a complete example of the use of the synchronous declarative language LUSTRE for the specification, description and verification of a resource arbiter, which is a regular network of hardware devices. The fact that both programs and properties may be expressed in LUSTRE is used to perform an inductive verification. An invariant property of the network is found, and merged with the description program. Verification is performed by model checking.