UNSPECIFIED (2004) On model checking data-independent systems with arrays without reset. In: 2nd International Workshop on Verification and Computational Logic (VCL 2001), Florence, ITALY, SEP 04, 2001. Published in: THEORY AND PRACTICE OF LOGIC PROGRAMMING, 4 (Part 5-6). pp. 659-693.

Full text not available from this repository.

Abstract

A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from Y. Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty finite instances of X and Y. Initially, we consider instead the abstraction where X and Y are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the mu-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of X and Y. We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the mu-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the mu-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where X is the type of memory addresses, and Y the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.

Item Type:	Conference Item (UNSPECIFIED)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Journal or Publication Title:	THEORY AND PRACTICE OF LOGIC PROGRAMMING
Publisher:	CAMBRIDGE UNIV PRESS
ISSN:	1471-0684
Date:	September 2004
Volume:	4
Number:	Part 5-6
Number of Pages:	35
Page Range:	pp. 659-693
Identification Number:	10.1017/S1471068404002054
Publication Status:	Published
Title of Event:	2nd International Workshop on Verification and Computational Logic (VCL 2001)
Location of Event:	Florence, ITALY
Date(s) of Event:	SEP 04, 2001
URI:	http://wrap.warwick.ac.uk/id/eprint/7875

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item