Show simple item record

dc.contributor.advisorBreugel, Franck van
dc.creatorShafiei, Nastaran
dc.description.abstractIn this dissertation, we focus on the verification of distributed Java applications composed of communicating multithreaded processes. We choose model checking as the verification technique. We propose an instance of the so-called centralization approach which allows for model checking multiple communicating processes. The main challenge of applying centralization is keeping data separated between different processes. In our approach, this issue is addressed through a new class-loading model. As one of our contributions, we implement our approach within an existing model checker, Java PathFinder (JPF). To account for interactions between processes, our approach provides the model checker with a model of interprocess communication. Moreover, our model allows for systematically exploring potential exceptional control flows caused by network failures. We also apply a partial order reduction (POR) algorithm to reduce the state space of distributed applications, and we prove that our POR algorithm preserves deadlocks. Furthermore, we propose an automatic approach to capture interactions between the system being verified and external resources, such as cloud computing services. The dissertation also discusses how our approach is superior to existing approaches. Our approach exhibits better performance which is mainly due to the POR technique. Furthermore, our approach allows for verifying a considerably larger class of applications without the need for any manual modeling, and it has been successfully used to detect bugs that cannot be found using previous work.
dc.rightsAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
dc.subjectComputer science
dc.subjectComputer engineering
dc.titleModel Checking of Distributed Multi-Threaded Java Applications
dc.typeElectronic Thesis or Dissertation Science - Doctor of Philosophy
dc.subject.keywordsPartial order reductionen_US
dc.subject.keywordsSoftware verificationen_US
dc.subject.keywordsModel checkingen_US
dc.subject.keywordsDistributed applicationen_US
dc.subject.keywordsJava PathFinderen_US
dc.subject.keywordsClass-loading modelen_US
dc.subject.keywordsNative callsen_US
dc.subject.keywordsState space reductionen_US

Files in this item


This item appears in the following Collection(s)

Show simple item record

All items in the YorkSpace institutional repository are protected by copyright, with all rights reserved except where explicitly noted.