Liu Yang's PhD Thesis
Title: Model Checking Concurrent and Real-time Systems: the PAT Approach
Thesis Draft Download
  • For Review Version (1.5 lined,11pt): PDF.
Thesis Talk Slides Download
  • For Oral Defence: PPT.
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.

  • We propose a unified on-the-fly model checking algorithm to handle a variety of fairness assumptions, which is further tuned to support parallel verification in multi-core architecture with shared memory. We apply the proposed algorithm on a set of self-stabilizing population protocols, which only work under global fairness. One previously unknown bug is discovered in a leader election protocol. Population protocols are designed for networks with large or even unbounded number of nodes, which gives the space explosion problem. To solve this problem, we develop a process counter abstraction technique to handle parameterized systems under fairness. We show that model checking under fairness is feasible, even without the knowledge of process identifiers.

  • Based on the ideas in FDR, we present a on-the-fly model checking algorithm for refinement checking, incorporated with advanced model checking techniques. This algorithm is successfully applied in automatic linearizability verification and conformance checking between Web Services.

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 main result of this thesis is Process Analysis Toolkit (PAT), a self-contained framework to support composing, simulating and reasoning of concurrent and real-time systems. PAT implements all proposed model checking techniques catering for checking deadlock-freeness, 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.

 

Publications from the Thesis
  1. Yang Liu, Jun Sun and Jin Song Dong. Scalable Multi-Core Model Checking Fairness Enhanced Systems. The 11th International Conference on Formal Engineering Methods (ICFEM 2009). Rio de Janeiro, Brazil, December, 2009. (Accepted).
  2. Jun Sun, Yang Liu, Jin Song Dong and Xian Zhang. Verifying Stateful Timed CSP using Implicit Clocks and Zone Abstraction. The 11th International Conference on Formal Engineering Methods (ICFEM 2009). Rio de Janeiro, Brazil, December, 2009. (Accepted).
  3. Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu and Jin Song Dong. Fair Model Checking of Parameterized Systems. The sixth International Symposium on Formal Methods (FM 2009). Eindhoven, the Netherlands, November, 2009. (Accepted).
  4. Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. Model Checking Lineariability via Refinement. The sixth International Symposium on Formal Methods (FM 2009). Eindhoven, the Netherlands, November, 2009. (Accepted).
  5. Yang Liu, Jun Pang, Jun Sun and Jianhua Zhao. Verification of Population Ring Protocols in PAT. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009). China.
  6. Jun Sun, Yang Liu, Jin Song Dong and Chun Qing Chen. Integrating Specification and Programs for System Modeling and Verification. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009). China.
  7. Shaojie Zhang, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen and Yanhong A. Liu. Formal Verification of Scalable NonZero Indicators. The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE 2009). pages 406-411, USA. 2009.
  8. Jun Sun, Yang Liu, Jin Song Dong and Jun Pang. Towards Flexible Verification under Fairness. The 21th International Conference on Computer Aided Verification (CAV 2009). pages 702-708, France, 2009.
  9. Jun Sun, Yang Liu, Jin Song Dong and Hai H. Wang. Specifying and Verifying Event-based Fairness Enhanced Systems. The 10th International Conference on Formal Engineering Methods (ICFEM 2008). Japan, 2008.
  10. Jun Sun, Yang Liu and Jin Song Dong. CSP Model Checking Revisited: Introducing a Process Analysis Toolkit. The third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008), Greece, October 13-15, 2008.
  11. Jun Sun, Yang Liu, Jin Song Dong and Jing Sun, Compositional Encoding for Bounded Model Checking. Frontiers of Computer Science in China, Nov, 2008.
  12. Jun Sun, Yang Liu and Jin Song Dong. Bounded Model Checking of Compositional Processes, 2nd IEEE & IFIP Theoretical Aspects of Software Engineering Conference (TASE 2008), NanJing, China, Jun. 2008.
  13. Yang Liu, Jun Sun and Jin Song Dong. An Analyzer for Extended Compositional Process Algebras, The 30th International Conference on Software Engineering (ICSE 2008), Germany, 2008.
  14. Jin Song Dong, Yang Liu, Jun Sun and Xian Zhang, Verification of Computation Orchestration via Timed Automata. 8th International Conference on Formal Engineering Methods (ICFEM'06), Macau, November 2006.

Last updated: 25/10/2009