Please use this identifier to cite or link to this item:
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.
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



Page view(s)

checked on May 17, 2019


checked on May 17, 2019

Google ScholarTM


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