A framework for compositional verification of multi-valued systems via abstraction-refinement

详细信息    查看全文

• 作者：Yael Meller^a ; ^{ymeller@cs.technion.ac.il" class="auth_mail" title="E-mail the corresponding author} ; Orna Grumberg^a ; ^{orna@cs.technion.ac.il" class="auth_mail" title="E-mail the corresponding author} ; Sharon Shoham^b ; ^{sharon.shoham@gmail.com" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Multi-valued model checking ; Mu-calculus ; Bilattices ; Mixed simulation ; Refinement ; Compositional model checking
• 刊名：Information and Computation
• 出版年：2016
• 出版时间：April 2016
• 年：2016
• 卷：247
• 期：Complete
• 页码：169-202
• 全文大小：1119 K

文摘

We present a framework for fully automated compositional verification of μ-calculus specifications over multi-valued systems, based on abstraction and refinement.

In a multi-valued model of a system, both the system transitions and the state labels are assigned values from a lattice. We formalize our framework based on bilattices, consisting of a truth lattice and an information lattice. Formulas are interpreted on the truth lattice. The information lattice determines how definite the value is, in terms of the concrete system being modeled.

Our compositional approach views each component as an abstraction of the entire system and checks it separately. Only if all individual checks return indefinite values, the parts of the components which are responsible for these values, are composed and checked. If the latter check is still indefinite, a refinement of the multi-valued system is needed. Refinement is aimed at increasing the information level of model details.