Translation-based compositional reasoning for software systems

Software systems are often model checked by translating them into a directly model-checkable formalism. Any serious software system requires application of compositional reasoning to overcome the computational complexity of model checking. This paper presents Translation-Based Compositional Reasoning (TBCR), an approach to application of compositional reasoning in the context of model checking software systems through model translation. In this approach, given a translation from a software semantics to a directly model-checkable formal semantics, a compositional reasoning rule is established in the software semantics and mapped to an equivalent rule in the formal semantics based on the translation. The correctness proof of the composition reasoning rule in the software semantics is established based on this mapping and the correctness proof of the equivalent rule in the formal semantics. The compositional reasoning rule in the software semantics is implemented and applied based on the translation from the software semantics to the formal semantics and reusing the implementation of the equivalent rule in the formal semantics. TBCR has been realized for a commonly used software semantics, the Asynchronous Interleaving Message-passing semantics. TBCR is illustrated by two applications of this realization.