The Library
Relating data independent trace checks in CSP with UNITY reachability under a normality assumption
Tools
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. ISBN 3-540-21377-5. ISSN 0302-9743.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Abstract
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 | ||||
Publisher: | SPRINGER-VERLAG BERLIN | ||||
ISBN: | 3-540-21377-5 | ||||
ISSN: | 0302-9743 | ||||
Editor: | Boiten, EA and Derrick, J and Smith, G | ||||
Official Date: | 2004 | ||||
Dates: |
|
||||
Volume: | 2999 | ||||
Number of Pages: | 20 | ||||
Page Range: | pp. 247-266 | ||||
Publication Status: | Published | ||||
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 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |