Lifting assertion and consistency checkers from single to multiple viewpoints

Abstract

Using a priority preorder on requirements or specifications, we lift established property-verification techniques of threevalued model checking from single to multiple viewpoints. This lift guarantees a maximal degree of autonomy and accountability to single views, automatically synthesizes single-analysis results for multiple-view consistency and assertion checking, allows the re-use of single-view technology (e.g. standard model checkers), and transforms many meta-results (e.g. soundness of abstraction) from the singleview to the multiple-view setting. We formulate assertionconsistency lattices as a proper denotational universe for this lift, show that their symmetric versions are DeMorgan lattices, and classify both structures through (idempotent) order-isomorphisms on (self-dual) priority preorders in the finite case. In particular, this lift generalizes Fitting’s multiple-valued semantics of modal logic in that our treatment of negation generalizes Heyting negation beyond fully specified and consistent models. We compare our approach to existing work on multiple-valued model checking.