Verifying systems with replicated components in Murϕ

Abstract

We present an extension to the Murϕ verifier to verify systems with replicated identical components. Verification is by explicit state enumeration in an abstract state space where states do not record the exact numbers of components. Through a new datatype, called Repetitive lD, the user can suggest the use of such an abstraction to verify a system of fixed size. Murϕ automatically checks the soundness of the abstract state graph, and automatically constructs the abstract state graph using the system description. Using a simple run time check, Murϕ can also determine if it can generalize the verification result of a system with fixed size to systems of larger sizes, including the system with infinite number of components.