Semantic preorders in the automated verification of concurrent systems
Ufuk Celikkan · 1996
Preorders are reflexive and transitive relations which are emerging as promising alternatives equivalences in system verification, since preorder-based specifications permit more flexibility in the implementations that are deemed correct. Preorder-based reasoning lets certain parts of a specification be left undefined therefore allowing latitude in the implementation strategy chosen. This partiality allowed in the specifications (and implementations) permits a form of stepwise refinement design methodology in designing correct implementations. Preorders formalize the intuitive notion of to be better than. A system is deemed be correct if it is larger than its specification in the preorder, in which case it intuitively provides at least the behavior dictated by the specification. Preorders, like their equivalence counterparts, facilitate the development of layered, hierarchical designs. They can also be used as a basis in the modular and compositional verification of systems. This thesis presents algorithms for computing a very general preorder--the prebisimulation preorder--and gives a methodology generate diagnostic information, when two systems are not related by the prebisimulation preorder. As a number of other behavioral preorders may be characterized in terms of prebisimulation preorder the algorithms presented in this thesis may be used as a basis for computing diagnostic information for these preorders as well. The diagnostic information takes the form of a logical formula which may be then transformed as appropriate in order yield information for the specific preorder being calculated. We illustrate this technique by presenting a method for generating diagnostic tests when two systems are not related by the testing preorder. The practicality of these techniques is also investigated by applying them verifying a simplified version of an ATM protocol.