Model Checking of Distributed Multi-Threaded Java Applications

Simple item page
dc.contributor.advisorBreugel, Franck van
dc.creatorShafiei, Nastaran
dc.date.accessioned2015-01-26T14:22:31Z
dc.date.available2015-01-26T14:22:31Z
dc.date.copyright2014-03-31
dc.date.issued2015-01-26
dc.date.updated2015-01-26T14:22:31Z
dc.degree.disciplineComputer Science
dc.degree.levelDoctoral
dc.degree.namePhD - Doctor of Philosophy
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.identifier.urihttp://hdl.handle.net/10315/28190
dc.language.isoen
dc.rightsAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
dc.subjectComputer science
dc.subjectComputer engineering
dc.subject.keywordsPartial order reductionen_US
dc.subject.keywordsSoftware verificationen_US
dc.subject.keywordsModel checkingen_US
dc.subject.keywordsDistributed applicationen_US
dc.subject.keywordsConcurrencyen_US
dc.subject.keywordsJavaen_US
dc.subject.keywordsJava PathFinderen_US
dc.subject.keywordsClass-loading modelen_US
dc.subject.keywordsNative callsen_US
dc.subject.keywordsState space reductionen_US
dc.titleModel Checking of Distributed Multi-Threaded Java Applications
dc.typeElectronic Thesis or Dissertation

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Shafiei_Nastaran_2014_PhD.pdf
Size:
3.36 MB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
license.txt
Size:
1.83 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
YorkU_ETDlicense.txt
Size:
3.38 KB
Format:
Plain Text
Description:
Download

Collections

Computer Science and Engineering

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