Please use this identifier to cite or link to this item:
Title: Model checking parameterized process classes
Keywords: Model checking, Parameterization, Process classes
Issue Date: 23-Jul-2009
Citation: 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.
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



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.