M.Sc Thesis

M.Sc StudentMeller Yael
SubjectMulti Valued Abstraction and Compositional Model Checking
DepartmentDepartment of Computer Science
Supervisor PROFESSOR EMERITUS Orna Grumberg
Full Thesis textFull thesis text - English Version


We present a framework for fully automated compositional verification of mu-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 construction 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 evaluated with respect to the truth lattice. On the other hand, refinement is now aimed at increasing the information level of model details, thus also increasing the information level of the model checking result. Based on the two lattices and on multi-valued model checking graphs, we suggest how multi-valued models should be composed, checked, and refined.