Report

### 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 bea...

### Authors

Publisher:
Oxford University Computing Laboratory
URN:
uuid:d0e0d198-e628-476b-a3e6-e477a83822ea
Local pid:
cs:928