IIIT Hyderabad Publications
Distributed Safety Verification Using Vertex Centric Programming Model
Authors: Adhish Singla Adhish Singla,Krishnaji Krishnaji Desai,Suresh Purini,Venkatesh Choppella
Conference: International Symposium on Parallel and Distributed Computing
Report no: IIIT/TR/2016/36
Software is finding place in deeply embedded systems to large scale distributed systems of cloud service providers such as Amazon and Google. Due to the concurrent and distributed nature of this software, it is hard to test for correctness of such systems in a foolproof manner. Explicit state model checking is an approach in which we build a model of the system and specify the properties it should hold. Then we construct a state transition system from the model and check if it satisfies the specified properties. There are two kinds of properties of interest: safety and liveness. In this paper, we focus our attention on safety verification, which involves checking if the states that are generated in the transition system satisfy some predicate formulae specified in the form of assertions. The main problem here is that the number of states in the transition system grows exponentially with the number of bits required to store the state of a model at any given point time. So the available main memory even in a server class machine is not sufficient to model check nontrivial practical models. One approach to address this problem is by using resources from a distributed collection of machines. In this paper, we adopt this approach, by proposing a distributed safety property verification algorithm using the vertex centric programming model.
Full paper: pdf
Centre for Software Engineering Research Lab
Copyright © 2009 - IIIT Hyderabad. All Rights Reserved.