A Framework For Compositional Verification of Multi-Valued Systems Via Abstraction-Refinement?

Abstract. We present a framework for fully automated compositional verifi-cation of µ-calculus specifications over multi-valued systems, based on multi-valued abstraction and refinement. Multi-valued models are widely used in many applications of model checking. They enable a more precise modeling of systems by distinguishing several levels of uncertainty and inconsistency. Successful verification tools such as STE (for hardware) and YASM (for software) are based on multi-valued models. Our compositional approach model checks individual components of a system. Only if all individual checks return indefinite values, the parts of the components which are responsible for these values, are composed and checked. Thus the con-struction of the full system is avoided. If the latter check is still indefinite, then a refinement is needed. We formalize our framework based on bilattices, consisting of a truth lattice and an information lattice. Formulas interpreted over a multi-valued model are eval-uated w.r.t. to the truth lattice. On the other hand, refinement is now aimed at increasing the information level of model details, thus also increasing the infor-mation level of the model checking result. Based on the two lattices, we suggest how multi-valued models should be composed, checked, and refined.