Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/16288
Title: Model checking parameterized process classes
Authors: LIU SHANSHAN
Keywords: Model checking, Parameterization, Process classes
Issue Date: 23-Jul-2009
Source: LIU SHANSHAN (2009-07-23). Model checking parameterized process classes. ScholarBank@NUS Repository.
Abstract: Systems consisting of large (or even unbounded) number of behaviorally similarprocesses communicating with each other are known as parameterized systems.Such systems are common in distributed computing and real-life software systems.Verifying properties for such systems involves reasoning about unboundedly manyprocesses and hence cannot be accomplished directly by model-checking.In this thesis, we present an abstraction re nement based veri cation frameworkfor parameterized systems. We enhance the well-known Spin model checker withprocess count abstraction to develop a time/memory e cient Linear-time TemporalLogic (LTL) veri er for parameterized systems. We also developed methods toautomatically detect spurious counter-examples and re ne the abstraction. The usability/ scalability of our checker is demonstrated via the modeling and automatedveri cation of several real-life parameterized control systems and protocols.
URI: http://scholarbank.nus.edu.sg/handle/10635/16288
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
LiuShanshan_MSc_thesis.pdf664.59 kBAdobe PDF

OPEN

NoneView/Download

Page view(s)

193
checked on Dec 11, 2017

Download(s)

144
checked on Dec 11, 2017

Google ScholarTM

Check


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