Show simple item record

dc.contributor.authorFarheen, Sabria 17:00:45 (GMT) 17:00:45 (GMT)
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.publisherUniversity of Waterlooen
dc.titleImprovements to Transitive-Closure-based Model Checking in Alloyen
dc.typeMaster Thesisen
dc.pendingfalse R. Cheriton School of Computer Scienceen Scienceen of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorDay, Nancy
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages