Extending A Model-Checking Tool With Non-trivial Data Structures

Model-checking is one of the most successful automatic verification techniques in the past two decades. It has been used in the analysis and verification of finite-state systems such as sequential circuit designs and communication protocols. Analyzing and verifying value-passing concurrent systems is a new research area in model-checking.With the rapid increase in the concurrent systems' scales, a challenging issue facing model-checking researchers is how to handle the huge state spaces. Thus it becomes increasingly important to develop suitable computation models and to design efficient verification algorithms. An important feature of value-passing systems concurrent is that it is always involving non-trivial data structures when several subsystems communicate with each other. Here, non-trivial data structures may include arrays, lists and records. The traditional approaches to handle non-trivial data structures are either abstracting them from system models or expanding them into non-structural data, which often reduces the efficiency of verification substantively. A possible solution to this problem is: adopting Symbolic Transition Graph with Assignment (STGA for short) to model value-passing systems, introducing a predicate mu-calculus to characterize desired properties, and verifying value-passing concurrent processes using an "on-the-fly" algorithm.This thesis presents a way to introduce non-trivial data structures into the solution mentioned above, which helps to extend its application domain. The work includes: Extending value-passing CCS to a system description language with strict typing rules; Extending accordingly the definition and generation rules of the basic STGA, which makes it suitable for modeling real systems. Presenting optimization algorithms for extended STGA Extending the syntax of the script language to definite the verification problem, and implementing the compilation and STGA generation module for this language; Incorporating the module with the core verification algorithm; demonstrating the validation and analyzing the performance of the tool with some real-world examples...