On model checking data-independent systems with arrays without reset

DOI10.1017/S1471068404002054zbMATH Open1088.68108arXivcs/0405103MaRDI QIDQ4669653FDOQ4669653

Authors: R. S. Lazić, Tom Newcomb, A. W. Roscoe 

Publication date: 15 April 2005

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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 nite 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 u-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 u-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 u-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.

Full work available at URL: https://arxiv.org/abs/cs/0405103

Recommendations

• Communicating Sequential Processes. The First 25 Years
• scientific article; zbMATH DE number 1759637
• Towards SMT Model Checking of Array-Based Systems
• scientific article; zbMATH DE number 2061713
• Algebraic Methodology and Software Technology

zbMATH Keywords

\(\mu\)-calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Cited In (6)

• On the decidability of the safety problem for access control policies
• Genericity and the \(\pi\)-calculus
• Communicating Sequential Processes. The First 25 Years
• A semantic condition for data independence and applications in hardware verification
• Title not available (Why is that?)
• Light-weight SMT-based model checking

This page was built for publication: On model checking data-independent systems with arrays without reset

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4669653)