Verifying Distributed Systems with Model Checking and Static Analysis
M.M. Gallardo and P. Merino
University of Malaga, SPAIN
Abstract
The purpose of verification of software for concurrent systems is to reduce
the risk of serious design errors produced by multiple processes that
interact simultaneously with one another. This paper describes a
methodology for helping users in the specification and automatic
verification of software for distributed systems. Our proposal is to
combine state space-based analysis (model checking) with static analysis
techniques such as abstract interpretation and partial evaluation. This
combination is useful for obtaining more information about the behavior of
a particular system by analyzing more abstract or more specialized versions
of the system. In the paper we present the overall methodology that is
being consider to implement different tools towards the model checker SPIN.
Keywords:
abstract interpretation, specialization, temporal logic, model
checking, SPIN