Improvements to Transitive-Closure-based Model Checking in Alloy

dc.contributor.authorFarheen, Sabria
dc.date.accessioned2018-01-19T17:00:45Z
dc.date.available2018-01-19T17:00:45Z
dc.date.issued2018-01-19
dc.date.submitted2018-01
dc.description.abstractModel checking, which refers to the verification of temporal properties of a transition system, is a common formal method for verifying models. Transitive-closure-based model checking (TCMC), developed by Vakili et al., is a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive closure (FOLTC). TCMC is an expression of the complete (i.e., unbounded) model checking problem for CTLFC as a set of constraints in FOLTC without induction, iteration, or invariants. TCMC has been implemented in the Alloy Analyzer. This thesis focuses on improving practical aspects of using TCMC in Alloy. We provide style guidelines for writing concise declarative models of transition systems for behavioural analysis in Alloy without any extensions to the Alloy language. We address the issue of spurious instances produced when generating instances at small scopes using the Alloy Analyzer by introducing significance axioms, which ensure the instance contains interesting behaviour. We define scoped TCMC for a state scope of n, where n is less than the size of the reachable state space, as the model checking of all transition system instances of state size n that satisfy the transition relation. By considering infinite and finite paths of a transition system separately, we can make useful deductions about the complete model checking problem from the results of scoped TCMC for certain categories of properties. The significant scope, derived from the significance axioms, provides a measure independent of computing resource limitations that a significant part of the state space has been verified, providing higher confidence in the deductions from scoped TCMC. We present case studies that demonstrate the claims and results of this work. We also compare TCMC in Alloy to NuSMV and bounded model checking in terms of modelling practices, expressibility of temporal properties, model checking results, and performance.en
dc.identifier.urihttp://hdl.handle.net/10012/12900
dc.language.isoenen
dc.pendingfalse
dc.publisherUniversity of Waterlooen
dc.titleImprovements to Transitive-Closure-based Model Checking in Alloyen
dc.typeMaster Thesisen
uws-etd.degreeMaster of Mathematicsen
uws-etd.degree.departmentDavid R. Cheriton School of Computer Scienceen
uws-etd.degree.disciplineComputer Scienceen
uws-etd.degree.grantorUniversity of Waterlooen
uws.contributor.advisorDay, Nancy
uws.contributor.affiliation1Faculty of Mathematicsen
uws.peerReviewStatusUnrevieweden
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.scholarLevelGraduateen
uws.typeOfResourceTexten

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Farheen_Sabria.pdf
Size:
1.25 MB
Format:
Adobe Portable Document Format
Description:

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
6.08 KB
Format:
Item-specific license agreed upon to submission
Description: