Please use this identifier to cite or link to this item: http://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
Source: 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)

117
checked on Dec 11, 2017

Download(s)

172
checked on Dec 11, 2017

Google ScholarTM

Check


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