Fast development of hardware/software design requires more versatile and powerful verification methods to help engineers understand, verify, and debug their systems. The scope of system verification now is not limited to finding functional errors at the logic level, but also includes analyzing and predicting the bottlenecks in performance and dependability. Model checking, which was originally proposed to verify discrete-state systems, has been further extended to the verification of probabilistic systems. Many techniques from other communities, such as Markov chain analysis, are involved in the model checking process. Traditional and new verification techniques must be integrated into a platform that can handle both the logic and probabilistic aspects of a given model.

Symbolic model checking using decision diagrams has achieved great success in verifying many practical software and hardware systems, and is still the primary approach to logic verification. Recent research shows that decision diagrams can be successfully employed in probabilistic model checking. This thesis is devoted to future improving the capability of decision diagram techniques in model checking. Specifically, this thesis explores the application of a family of decision diagrams, including multi-way decision diagrams and edge-valued multi-way decision diagrams, to several topics in both classic and probabilistic model checking.

My thesis consists of two parts of work: In the first part, I extend the existing saturation algorithm, which was originally proposed for state-space generation, to CTL model checking, strongly-connected component enumeration, and shortest witness generation for various properties. The second part of the thesis focuses on probabilistic model checking using decision diagrams. I propose a new and more efficient algorithm to carry out the Gauss-Seidel iterative method, which is a key step in probabilistic model checking. This technique can be applied to both steady-state solution of continuous-time Markov chains and CSL model checking. Then, I introduce a new bounding semantics of CSL to tackle truncation errors in numerical analysis and correctly evaluate nested CSL formulas.

The proposed techniques have been integrated into the SMART tool developed in our lab. Experimental results demonstrate that SMART is a promising platform to handle both logic and quantitative verification for many practical systems.

Hybrid systems tightly integrate software-based discrete control systems and continuous physical phenomena. Better methods and tools for design, modeling, and analysis are necessary as these systems become more complex, powerful, and prevalent in our daily life. There are two main approaches to model hybrid systems. One is to discretize them into fully discrete systems. We focus on two discrete models: a network of communicating FSMs (NCFSM) and event-condition-action (ECA) rules. In this dissertation, we make several contributions to verifying discrete systems. First, for an NCFSM, we symbolically encode and verify the properties of livelocks, strong connectedness, and dead transitions. We also design a symbolic equivalence checker to automatically generate test cases for fault-based testing. Second, for ECA rules, we verify both termination and confluence properties and then provide the first practical experimental results for the confluence property.

The second modeling method is to keep the continuous dynamics by using hybrid automata or block diagrams. Most verification problems for hybrid automata are undecidable even under severe limitations. However, using block diagrams, such as Simulink, researchers model a hybrid system as an input-output signals mapping box. This approach has been widely adopted by industry due to its scalability. Combining simulation and temporal logic, the validation technique is able to check whether the temporal behavior of the system meets a set of requirements. One significant challenge to the formal validation is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. In this dissertation, we make the following contributions to tackle the requirement defects. First, we compare the performance of the two existing falsification engines. Second, we design a requirement mining framework, an instance of counterexample-guided inductive synthesis, which is able to mine formal requirements from a closed-loop model. Third, we observe the importance of the monotonicity of formulas for synthesis and use a satisfiability modulo theories (SMT) solver to prove this property. Fourth, we propose weighted temporal logics to improve the performance of this mining framework. This framework has the following two applications: mined requirements can be used to validate future modifications of the model and enhance understanding of legacy models; the framework can also guide the process of bug-finding through simulations. We present two case studies for requirement mining: a simple automobile transmission controller and an industrial airpath control engine.

Symbolic verification has received much attention from both academia and industry in the past two decades. In particular, techniques based on decision diagrams have been successfully applied to various asynchronous and synchronous models.

Decision diagrams can compactly encode sets and relations, or vectors and matrices. For canonicity, variables associated to the nodes must be found in a predefined order on any path from the root, and duplicate nodes cannot be present. In addition, a reduction rule is enforced, the simplest being the quasi-reduced rule, where no variable is ever skipped. However, more efficient rules exist, where edges skip redundant nodes. With the fully-reduced rule, a node is redundant if all its outgoing edges point to the same node. With the zero-suppressed rule, a node is redundant if only its 0-edge is not pointing to a pre-defined default terminal node. None of these rules, however, is particularly effective when encoding transition relations of asynchronous systems or rate matrices of Markov models. We then introduce an identity-reducedrule, which generalizes Kronecker encodings to take advantage of state variables that remain unchanged after an event occurrence, and a c-reducedrule, which generalizes the zero-suppressed rule, and propose a new generally-reduced form of decision diagrams where each variable uses a specific reduction rule. We then illustrate the effectiveness of this new canonical form of decision diagrams with a wide set of applications.

State-space generation is usually the first and fundamental step for symbolic verification. Generally-reduced decision diagrams allow a more efficient symbolic state-space generation for general asynchronous systems by allowing on-the-fly extension of the state variable domains. After implementing both breadth-first and saturation-based state-space generation with this new data structure, we are able to exhibit substantial efficiency improvements with respect to traditional decision diagrams. Since previous works demonstrated that saturation outperforms breadth-first approaches, saturation with this new structure is now arguably the

state-of-the-art algorithm for symbolic state-space generation of asynchronous systems. When state-space generation completes, we also obtain the complete transition relation which can be used for

further analysis.

For synchronous systems, we study a type of timed Petri nets, which extends the traditional Petri nets to explicitly include real time in the model. We consider two fundamental reachability problems for timed Petri nets with positive integer firing times: timed reachability (find all markings where the model can be at a given finite time) and earliest reachability (find the minimum time when each reachable marking is entered). For these two problems, we define efficient symbolic algorithms that make use of both

generally-reduced decision diagrams without edge value and edge-valued decision diagrams, which associate integer value to the edges of decision diagrams. Runtime results on an extensive suite of models are provided to show the effectiveness and capability of our algorithm to cope with large state spaces.

Then, we study the use of decision diagrams in stochastic models. We present a new type of edge-valued decision diagrams which can be used to encode non-negative real-valued functions. We then utilize it in a new approximate numerical solution algorithm for general structured ergodic models. The approximation uses a state-space encoding provided by decision diagrams and a transition rate matrix encoding provided by these new edge-valued decision diagrams. The new method retains the favorable properties of a previously proposed Kronecker-based approximation, while eliminating the need for a Kronecker-consistent model decomposition. Removing this restriction allows for a greater utilization of event locality, which facilitates both state-space generation and transition rate matrix generation, thus extends the applicability of this algorithm to larger and more complex models.

All these algorithms are implemented based on our newly-designed Decision Diagram Library (DDL), which provides a user-friendly interface to create and manipulate generally-reduced decision diagrams with or without edge value It is the first library written for this purpose. This library is written in C++ and we adopt smart pointers for decision diagram node interface, similar to those in the Boost libraries, which automatically handle reference counts and garbage collection; this technique prevents memory leak and simplifies the interface, which greatly facilitate library users.

All above algorithms are integrated into our verification tool Smart version 2.

Motivation

Results

Availability and implementation

Contact

Supplementary information