Using probabilistic model checking for dynamic power management

Dynamic power management (DPM) refers to the use of runtime strategies in order to achieve a tradeoff between the performance and power consumption of a system and its components. We present an approach to analysing stochastic DPM strategies using probabilistic model checking as the formal framework. This is a novel application of probabilistic model checking to the area of system design. This approach allows us to obtain performance measures of strategies by automated analytical means without expensive simulations. Moreover, one can formally establish various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy.Received November 2003Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

Mu-calculus path checking

We investigate the path model checking problem for the μ-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the μ-calculus.     

State-rich model checking

In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more powerful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle state-rich systems specified using a combination of Z and CSP.     

Coverage metrics for temporal logic model checking*

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proved to be correct, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. In this paper we study coverage metrics for model checking. Coverage metrics are based on modifications we apply to the system in order to check which parts of it were actually relevant for the verification process to succeed. We introduce two principles that we believe should be part of any coverage metric for model checking: a distinction between state-based and logic-based coverage, and a distinction between the system and its environment. We suggest several coverage metrics that apply these principles, and we describe two algorithms for finding the non-covered parts of the system under these definitions. The first algorithm is a symbolic implementation of a naive algorithm that model checks many variants of the original system. The second algorithm improves the naive algorithm by exploiting overlaps in the variants. We also suggest a few helpful outputs to the user, once the non-covered parts are found.

A quadratic-time DBM-based successor algorithm for checking timed automata

Most of the timed automaton model checking algorithms explore state spaces by enumeration of time zones. The data structure called Difference Bound Matrix (DBM) is widely adopted to represent time zones because of its efficiency and simplicity. In this paper, we first present a quadratic-time algorithm to compute the canonical form of the conjunction of a canonical DBM and a time guard or a location invariant. Based on this algorithm, we present a quadratic-time DBM-based successor algorithm for timed automaton model checking.     

A tool supporting efficient model checking of concurrent specifications

We show a tool supporting efficient model checking of LOTOS programs. LOTOS is a well-known specification language for concurrent and distributed systems. The main functionality of the tool is the syntactic reduction of a program with respect to a logic formula expressing a property to be checked. The method is useful to reduce the state-explosion problem in model checking. The tool is integrated with the Concurrency Workbench of North Carolina. The tool also supports a windows user interface.     

Improving state class constructions for CTL* model checking of time Petri nets

The state space explosion is still one of the most challenging problems in formal verification using enumerative techniques. The challenge is even greater for real time systems whose state spaces are generally infinite due to time density. To use enumerative techniques with these systems, their state spaces need to be contracted into finite structures that preserve properties of interest. We propose in this paper an efficient approach to construct a contraction of the time Petri net model state space, which preserves its CTL* properties.     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.     

Model checking: a hardware design perspective

Current practices in the verification of commercial hardware designs (digital, synchronous, and sequential semiconductors) are described. Recent advances in verification by the mathematical technique called model checking are described, and requirements for the successful application of model checking in commercial design are discussed.     

Efficient reduction of finite state model checking to reachability analysis

Two types of temporal properties are usually distinguished: safety and liveness. Recently we have shown how to verify liveness properties of finite state systems using safety checking. In this article we extend the translation scheme to typical combinations of temporal operators. We discuss optimizations that limit the overhead of our translation. Using the notions of predicated diameter and radius we obtain revised bounds for our translation scheme. These notions also give a tight bound on the minimal completeness bound for simple liveness properties. Experimental results show the feasibility of the approach for complex examples. For one example, even an exponential speedup can be observed.     

OFMC: A symbolic model checker for security protocols

We present the on-the-fly model checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy data types as a simple way of building efficient on-the-fly model checkers for protocols with very large, or even infinite, state spaces. The second is the integration of symbolic techniques and optimizations for modeling a lazy Dolev–Yao intruder whose actions are generated in a demand-driven way. We present both techniques, along with optimizations and proofs of correctness and completeness.Our tool is state of the art in terms of both coverage and performance. For example, it finds all known attacks and discovers a new one in a test suite of 38 protocols from the Clark/Jacob library in a few seconds of CPU time for the entire suite. We also give examples demonstrating how our tool scales to, and finds errors in, large industrial-strength protocols.     

Partial-order reduction and trail improvement in directed model checking

In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search to improve the error-detection capabilities of explicit-state model checking. We first present the use of directed explicit-state model checking to improve the length of already established error trails. Second, we show that partial-order reduction, which aims at reducing the size of the state space by exploiting the commutativity of concurrent transitions in asynchronous systems, can coexist well with directed explicit-state model checking. Finally, we illustrate how to mitigate the excessive length of error trails produced by partial-order reduction in explicit-state model checking. In this context we also propose a combination of heuristic search and partial-order reduction to improve the length to already provided counterexamples.     

On model checking multiple hybrid views

Many applications, for instance the MS .NET Global Assembly Cache (GAC), are naturally expressed as 3-valued models where an additional third truth value models uncertainty or under-specification. An example of under-specification is that a component in a GAC may or may not have a main method. Models described in this manner can then be analyzed to refute or verify properties about the concrete systems they intend to model. This approach to system validation traditionally considers only one model at a time, even though this model may evolve if subjected to analysis. Many applications, however, benefit from or require the simultaneous consideration of multiple models of systems. We mention here requirements from different stake holders, and data drawn from federated databases.     

Heuristics for model checking Java programs

Model checking of software programs has two goals – the verification of correct software and the discovery of errors in faulty software. Some techniques for dealing with the most crucial problem in model checking, the state space explosion problem, concentrate on the first of these goals. In this paper we present an array of heuristic model checking techniques for combating the state space explosion when searching for errors. Previous work on this topic has mostly focused on property-specific heuristics closely related to particular kinds of errors. We present structural heuristics that attempt to explore the structure (branching structure, thread interdependency structure, abstraction structure) of a program in a manner intended to expose errors efficiently. Experimental results show the utility of this class of heuristics. In contrast to these very general heuristics, we also present very lightweight techniques for introducing program-specific heuristic guidance.     

Boolean and Cartesian abstraction for model checking C programs

We show how to attack the problem of model checking a C program with recursive procedures using an abstraction that we formally define as the composition of the Boolean and the Cartesian abstractions. It is implemented through a source-to-source transformation into a Boolean C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.     

Model checking of healthcare domain models

This paper shows the application of a type of formal software verification technique known as lightweight model checking to a domain model in healthcare informatics in general and public health surveillance systems in particular. One of the most complex use cases of such a system is checked using assertions to verify one important system property. This use case is one of the major justifications for the complexity of the domain model. Alloy Analyzer verification tool is utilized for this purpose. Such verification work is very effective in either uncovering design flaws or in providing guarantees on certain desirable system properties in the earlier phases of the development lifecycle of any critical project.     

CSL model checking algorithms for QBDs

We present an in-depth treatment of model checking algorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic stopping criterion, the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.     

A vertex centric parallel algorithm for linear temporal logic model checking in Pregel

Linear Temporal Logic (LTL) Model Checking is a very important and popular technique for the automatic verification of safety-critical hardware and software systems, aiming at ensuring their quality. However, it is well known that LTL model checking suffers from the state explosion problem, often leading to insurmountable scalability problems when applying it to real-world systems. While there has been work on distributed algorithms for explicit on-the-fly LTL model checking, these are not sufficiently scalable and capable of tolerating faults during computation, significantly limiting their usefulness in huge cluster environments. Moreover, implementing these algorithms is generally viewed as a very challenging, error-prone task. In this paper, we instead rely on Pregel, a simple yet powerful model for distributed computation on large graphs. Pregel has from the start been designed for efficient, scalable and fault tolerant operation on clusters of thousands of computers, including large cloud setups. To harness Pregel’s power, we propose a new vertex centric distributed algorithm for explicit LTL model checking of concurrent systems. Experimental results illustrate feasibility and scalability of the proposed algorithm. Compared with other distributed algorithms, our algorithm is more scalable, reliable and efficient.     

基于模型检测的硬件木马检测技术研究

硬件木马对原始电路的恶意篡改,已成为集成电路面临的核心安全威胁.为了保障集成电路的安全可信,研究人员提出了诸多硬件木马检测方法.其中,模型检测作为一种形式化验证方法,在设计阶段可有效检测出硬件木马.首先,阐述了模型检测的工作原理和应用流程;其次,介绍了基于模型检测的硬件木马检测技术的研究进展;最后,指出了当前该技术所面...     

Application of static analyses for state-space reduction to the microcontroller binary code

This paper describes the application of two abstraction techniques, namely dead variable reduction and path reduction, to the microcontroller binary code in order to tackle the state-explosion problem in model checking. These abstraction techniques are based on static analyses, which have to cope with the peculiarities of the binary code such as hardware dependencies, interrupts, recursion, and globally accessible memory locations. An interprocedural static analysis framework is presented that handles these peculiarities. Based on this framework, extensions of dead variable reduction and path reduction are detailed. A case study using several microcontroller programs is presented in order to demonstrate the efficiency of the described abstraction techniques.