Relating data independent trace checks in CSP with UNITY reachability under a normality assumption
UNSPECIFIED (2004) Relating data independent trace checks in CSP with UNITY reachability under a normality assumption. In: 4th International Conference on Integrated Formal Methods (IFM 2004), Canterbury, ENGLAND, APR 04-07, 2004. Published in: INTEGRATED FORMAL METHODS, PROCEEDINGS, 2999 pp. 247-266.Full text not available from this repository.
This paper shows how to translate the problem of deciding trace refinement between two data independent (DI) CSP processes to an unreachability problem in a DI Unity program. We cover here the straightforward but practically useful case when the specification satisfies a normality condition, Norm, meaning that we do not have to worry about hidden or unrecorded(1) data variables. This allows us to transfer results about the decidability of verification problems involving programs with data independent arrays from UNITY to CSP.
|Item Type:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||LECTURE NOTES IN COMPUTER SCIENCE|
|Journal or Publication Title:||INTEGRATED FORMAL METHODS, PROCEEDINGS|
|Editor:||Boiten, EA and Derrick, J and Smith, G|
|Number of Pages:||20|
|Page Range:||pp. 247-266|
|Title of Event:||4th International Conference on Integrated Formal Methods (IFM 2004)|
|Location of Event:||Canterbury, ENGLAND|
|Date(s) of Event:||APR 04-07, 2004|
Actions (login required)