The Library
On model checking dataindependent systems with arrays without reset
Tools
UNSPECIFIED (2004) On model checking dataindependent 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 56). pp. 659693. ISSN 14710684. doi:10.1017/S1471068404002054
Full text not available from this repository, contact author.
Official URL: http://dx.doi.org/10.1017/S1471068404002054
Abstract
A system is dataindependent 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 dataindependent 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 modelchecking problem: whether a given program satisfies a given temporallogic formula for all nonempty 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 dataindependent systems without arrays, we show that the mucalculus modelchecking 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 modelchecking problem of the universal fragment of the mucalculus, such that it always terminates but may give false negatives. We also deduce that the parameterised modelchecking problem of the universal disjunctionfree fragment of the mucalculus is decidable. Practical motivations for model checking dataindependent 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 faulttolerant 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:  14710684  
Official Date:  September 2004  
Dates: 


Volume:  4  
Number:  Part 56  
Number of Pages:  35  
Page Range:  pp. 659693  
DOI:  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 
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 