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), APR 04-07, 2004, Canterbury, ENGLAND.

Full text not available from this repository.

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
Date:	2004
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
URI:	http://wrap.warwick.ac.uk/id/eprint/8446

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item