Please use this identifier to cite or link to this item:
|Title:||Model checking concurrent and real-time systems : the PAT approach||Authors:||LIU YANG||Keywords:||Formal Verification, Concurrent and Real-time Systems, Model Checking, PAT||Issue Date:||26-Oct-2009||Citation:||LIU YANG (2009-10-26). Model checking concurrent and real-time systems : the PAT approach. ScholarBank@NUS Repository.||Abstract:||The design and verification of
concurrent and real-time systems are notoriously difficult problems.
Among the software validation techniques, model checking approach
has been proved to be successful as an automatic and effective
solution. In this thesis, we study the verification of concurrent
and real-time systems using model checking approach.
First, we design an integrated formal language for concurrent and real-time modeling, which combines high-level specification languages with mutable data variables and low-level procedural codes for the purpose of efficient system analysis, in particular, model checking. Timing requirements are captured using behavior patterns like deadline, time out, etc. A formal semantic model is defined for this language.
Based on this modeling language, we investigate LTL verification problem with focus of fairness assumptions, and refinement checking problem with following results.
Symbolic model checking is capable of handling large state space. We present an alternative solution for LTL verification using bounded model checking approach. Hierarchical systems are encoded as SAT problems. The encoding avoids exploring the full state space for complex systems so as to avoid state space explosion.
To support verification of real-time systems, we propose an approach using a fully automated abstraction technique to build an abstract finite state machine from the real-time model. We show that the abstraction has finite state and is subject to model checking. Furthermore, it weakly bi-simulates the concrete model and we can perform LTL model checking, refinement checking and even timed refinement checking upon the abstraction.
The results of this thesis are embodied in the design and implementation of a self-contained framework: Process Analysis Toolkit (PAT), which supports composing, simulating and reasoning of concurrent and real-time systems. This framework includes all of the proposed techniques: deadlock-freedom, reachability, LTL checking, refinement checking and etc. PAT adopts an extensible design, which allows new languages and verification algorithms to be supported easily. Currently, three modules have been developed in PAT. The experiment results show that PAT is capable of verifying systems with large number of states and complements the state-of-the-art model checkers in several aspects.
|Appears in Collections:||Ph.D Theses (Open)|
Show full item record
Files in This Item:
|LiuY.pdf||1.66 MB||Adobe PDF|
checked on Apr 18, 2019
checked on Apr 18, 2019
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.