Translating CSP trace refinement to UNITY unreachability : a study in data independence
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 s...
| Main Authors: | , , |
|---|---|
| Format: | Report |
| Published: |
Oxford University Computing Laboratory
2015
|
| _version_ | 1797096204720406528 |
|---|---|
| author | Roscoe, A Wang, X Lazic, R |
| author_facet | Roscoe, A Wang, X Lazic, R |
| author_sort | Roscoe, A |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T04:38:44Z |
| format | Report |
| id | oxford-uuid:d0e0d198-e628-476b-a3e6-e477a83822ea |
| institution | University of Oxford |
| last_indexed | 2024-03-07T04:38:44Z |
| publishDate | 2015 |
| publisher | Oxford University Computing Laboratory |
| record_format | dspace |
| spelling | oxford-uuid:d0e0d198-e628-476b-a3e6-e477a83822ea2022-03-27T07:53:13ZTranslating CSP trace refinement to UNITY unreachability : a study in data independenceReporthttp://purl.org/coar/resource_type/c_93fcuuid:d0e0d198-e628-476b-a3e6-e477a83822eaDepartment of Computer ScienceOxford University Computing Laboratory2015Roscoe, AWang, XLazic, RThis 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. |
| spellingShingle | Roscoe, A Wang, X Lazic, R Translating CSP trace refinement to UNITY unreachability : a study in data independence |
| title | Translating CSP trace refinement to UNITY unreachability : a study in data independence |
| title_full | Translating CSP trace refinement to UNITY unreachability : a study in data independence |
| title_fullStr | Translating CSP trace refinement to UNITY unreachability : a study in data independence |
| title_full_unstemmed | Translating CSP trace refinement to UNITY unreachability : a study in data independence |
| title_short | Translating CSP trace refinement to UNITY unreachability : a study in data independence |
| title_sort | translating csp trace refinement to unity unreachability a study in data independence |
| work_keys_str_mv | AT roscoea translatingcsptracerefinementtounityunreachabilityastudyindataindependence AT wangx translatingcsptracerefinementtounityunreachabilityastudyindataindependence AT lazicr translatingcsptracerefinementtounityunreachabilityastudyindataindependence |