Translating CSP trace refinement to UNITY unreachability : a study in data independence

Abstract

This paper tries to translate trace refinement between CSP processes to unreachability on Unity-like languages. The key concern, however, is on how data independent (DI) variables and DI arrays could be treated in the translation. It proves to be a challenging task since CSP can utilize DI data in some subtle ways which cannot be simulated in Unity. To solve the problem, we find an interesting subclass of CSP specifications called DI-explicit specifications. This notion of DI-explicitness bears out to be the necessary condition for translatability, based on which a formal translation procedure is formulated for trace refinement checking problem. Using the semantic constructs of partitions and decorations, the translation is proved to be correct and some extensions are discussed. Overall, this paper is a first step to build a bridge from our recent DI array work in Unity-like languages to our previous DI work in CSP. The main contribution of paper lies in identifying the right condition, framework and mathematical constructs to do the work.