Please use this identifier to cite or link to this item: https://scholarbank.nus.edu.sg/handle/10635/48323
Title: Cell : A compositional verification framework
Authors: JI KUN
Keywords: Formal Verification, Model Checking, Compositional Verification,Concurrent System, Real-time System, CELL Framework
Issue Date: 20-Jun-2013
Citation: JI KUN (2013-06-20). Cell : A compositional verification framework. ScholarBank@NUS Repository.
Abstract: Compositional techniques such as Assume-Guarantee Reasoning (AGR) are believed to be promising ways to alleviate the state space explosion problem associated with model checking in the ?divide-and-conquer" style. In this thesis, we present a comprehensive and extensible framework, namely CELL, to facilitate compositional verification of concurrent and real-time systems based on commonly used semantic models. For each semantic model, CELL offers three libraries, i.e., compositional verification paradigms, learning algorithms and model checking methods to support various state-of-the-art compositional verification approaches. With well-defined APIs, the framework could be applied to manufacture customized model checkers. In addition, we also present a compositional verification technique that is included in the framework namely Assume-Guarantee Abstraction Refinement (AGAR) for real-time systems, which is to apply AGAR compositional verification paradigm on real-time systems. In this thesis, we will show the detailed algorithm and prove the correctness and termination of it.
URI: http://scholarbank.nus.edu.sg/handle/10635/48323
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
jikun_thesis.pdf1.13 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

149
checked on May 17, 2019

Download(s)

192
checked on May 17, 2019

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.