Probabilistic Model Checking of Randomized Java Code

Simple item page
dc.contributor.advisorvan Breugel, Franck
dc.contributor.authorFatmi, Syyeda Aamina Zainab
dc.date.accessioned2021-07-06T12:43:54Z
dc.date.available2021-07-06T12:43:54Z
dc.date.copyright2020-09
dc.date.issued2021-07-06
dc.date.updated2021-07-06T12:43:54Z
dc.degree.disciplineElectrical and Computer Engineering
dc.degree.levelMaster's
dc.degree.nameMASc - Master of Applied Science
dc.description.abstractJava PathFinder (JPF) and PRISM are the most popular model checkers for Java code and systems that exhibit random behaviour, respectively. JPF, in combination with its extension jpf-probabilistic, extracts the underlying Markov chain of randomized Java code. We developed a new extension of JPF, called jpf-label, which provides users with an easy way to label the states of this Markov chain. Furthermore, we implemented a converter that leads to the first model checking tool that can check probabilistic properties of randomized algorithms implemented in Java, by making it possible to use JPF in conjunction with PRISM. Probabilistic bisimilarity is a technique used to minimize the state space of a labelled Markov chain in order to combat the state space explosion. We implemented three known algorithms to compute probabilistic bisimilarity for labelled Markov chains. We boosted the performance of these algorithms by improving those areas of the code which are most frequently executed. Moreover, we compared the practical running time and memory consumption of these algorithms with PRISM's.
dc.identifier.urihttp://hdl.handle.net/10315/38445
dc.languageen
dc.rightsAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
dc.subjectComputer science
dc.subject.keywords(probabilistic) model checking
dc.subject.keywordsJava PathFinder
dc.subject.keywordsPRISM
dc.subject.keywordsprobabilistic bisimilarity
dc.subject.keywordslabelled Markov chain
dc.titleProbabilistic Model Checking of Randomized Java Code
dc.typeElectronic Thesis or Dissertation

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Fatmi_Syyeda_Z_2020_Masters.pdf
Size:
1.49 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
license.txt
Size:
1.87 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
YorkU_ETDlicense.txt
Size:
3.39 KB
Format:
Plain Text
Description:
Download

Collections

Electrical and Computer Engineering

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