IIIT Hyderabad Publications |
|||||||||
|
Scalable Distributed Safety Verification using Actor ArchitectureAuthor: Adhish Singla Adhish Singla Date: 2019-12-13 Report no: IIIT/TH/2019/131 Advisor:Suresh Purini,Venkatesh Choppella AbstractSoftware is finding place in deeply embedded systems to large scale distributed systems of cloud service providers such as Amazon and Google. Due to concurrent and distributed nature of this software, it is hard to test for correctness of such systems in a foolproof manner. Model checking is now a standard technology for verifying large and complex systems. 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. The scaling of model checking, however, remains a significant challenge. Distributed model checking is an important and promising approach to tackle the problem of scale. In this thesis, we focus our attention on safety properties verification, which involves checking if the states that are generated in the transition system satisfies 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 of time. So the available main memory even in a server class machine is not sufficient to model check non-trivial practical models. One approach to address this problem is by using resources from a distributed collection of machines. We use two different distributed models in order to achieve the above mentioned. Our first implementation is based on vertex centric programming model. It is uses the concept of bulk synchronous parallel computing to synchronize. The second implementation uses Actor Model. We propose asynchronous algorithms for the verification and a simple reduction strategy in this implementation. The main advantage of Actor model is that it comes with a transparent way to scale from a single node to multiple nodes, without having to change any of the implementation. Full thesis: pdf Centre for Software Engineering Research Lab |
||||||||
Copyright © 2009 - IIIT Hyderabad. All Rights Reserved. |