کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426727 | 686250 | 2016 | 34 صفحه PDF | دانلود رایگان |
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.
Journal: Information and Computation - Volume 247, April 2016, Pages 169–202