Frontier Visionary Interview for hardware, software, system related business and and academia
Frontier Journal (FJ):
In 1981, you and Allen Emerson working in the U.S., and Joseph Sifakis working independently in France with J.P. Queille, authored seminal papers that founded what has become the highly successful field of Model Checking, which made you eventually co-winning the Turing Award. Could you provide us some historical briefing on that?
Edmund M. Clarke (EMC):
Model checking did not arise in a historical vacuum. There was an important problem that needed to be solved, namely Concurrent Program Verification. Concurrency errors are particularly difficult to find by program testing, since they are often hard to reproduce. Most of the formal research on this topic involved constructing a proof by hand using a Floyd-Hoare style logic. Probably, the best known formal system was the one proposed by Owicki and Gries for reasoning about Conditional Critical Regions. Although I had written my thesis on the meta-theory of Hoare Logic and was very familiar with the Owick-Gries proof methodology, I was quite skeptical about the scalability of hand-constructed proofs. There had been some practical research on state exploration methods for communication protocols by Gregor Bochmann and others, but the formal verification community largely ignored it. Also, in the late 1970¡¯s, Pnueli, followed by Owicki and Lamport, had proposed the use of temporal logic for specifying concurrent programs. Although they still advocated hand-constructed proofs, their work demonstrated convincingly that temporal logic was ideal for expressing concepts like mutual exclusion, absence of deadlock, and absence of starvation.
FJ:
In your co-authored book titled Model Checking, you stated applying model checking to a design consists of several tasks, namely Modeling, Specification and Verification (Implementation). Which one among those three are the most important factor in tackling today¡¯s verification challenge due to design¡¯s size and complexity explosion?
EMC:
All three are important, but the ¡°state explosion problem¡± in model checking is definitely the most important, since it limits the size of the examples that can be handled in practice. Developing techniques for overcoming the state explosion problem has been the driving force in model checking research during the past 28 years. Symbolic Model Checking using Ordered Binary Decision Diagrams, the Partial Order Reduction, Bounded Model Checking using fast propositional satisfiability solvers, and Counterexample Guided Abstraction Refinement (CEGAR) were all developed to overcome this problem.
FJ:
A system can be hardware, software, or hardware/software. System modeling involves with both functional modeling and timing modeling, which relate with computation model (e.g., Data-flow-oriented vs. Control-flow-oriented, Uni-processing vs. Multi-processing), time model (e.g., Continuous vs. Discrete, Time vs. Untimed, Cycle-based vs. Non-cycle-based, State-based vs. Event-driven, Branching-time vs. Linear-time, Single-rate vs. Multi-rate) and communication model (e.g. Shared Variable vs. Messaging Passing). What is your perspective on the impact of system modeling on formal verification?
EMC:
Model checking works best for systems that are finite state or have finite state abstractions. In practice, this means that model checking is most useful for systems that are control-dominated or in which control and data can be cleanly separated. If this is not the case, then abstraction may be necessary to eliminate the state explosion caused by complex data structures.
Compositional reasoning is also important for dealing with the complexity of model checking. Often it is useful to decompose a complex system into simpler parts, check each part separately, and use this information to conclude a global property of the complete system. A model of computation that facilitates this style of reasoning is clearly advantageous.
FJ:
A system model to be verified can be specified in different ways through the choice of specification languages. Any specification language has its syntax and semantics. Between syntax and semantics, which one do you think is more critical to the success of verification (implementation)? Among currently available verification specification languages (both text-based and graphic-based, e.g., CTL, LTL, mu-calculus, StateCharts), which one is the most suitable specification language if any to modern hardware verification based on model checking?
EMC:
I regard StateCharts as an extraordinarily useful notation for specifying systems to be verified, not properties. A number of model checkers have been written for StateCharts. Mu-calculus theory underlies both CTL and LTL model checking. It is very expressive, but formulas with more than two alternations of least and greatest fixpoint operators are difficult to understand. Obtaining good bounds on the complexity of mu-calculus model checking is an area of research (it is known to be in the intersection of NP and Co-NP). In my opinion, the mu-calculus is primarily of theoretical interest. Practical specification languages usually involve some combination of CTL, LTL, and omega-automata. One such language PSL (Property Specification Language) has been widely adopted by the semiconductor industry.
FJ:
Verifying any specified non-trivial system is inherently computationally hard in terms of running time complexity. There are quite a few ways in reducing model checking¡¯s running time complexity: e.g., problem space transformation through partial order reduction, symmetry exploitation, abstraction or approximation, trade-off memory complexity for running time complexity through BDD-based symbolic checking or SAT-based satisfiability checking, just to name a few. Based on your observation, how shall we leverage the power of novel algorithms and efficient data structure in tackling today¡¯s verification challenge due to design¡¯s size and complexity explosion?
EMC:
I think you have correctly identified the key problem in research on model checking: How to ¡°leverage the power of novel algorithms and efficient data structures in tackling today¡¯s verification challenges due to design¡¯s size and complexity explosion¡±. There are entire conferences (e.g., CAV, TACAS, etc.) and several books devoted to research on this problem. Summarizing even a few of the possible directions would require a much longer article and several weeks to write.
FJ:
Model checking is the process of checking whether a given structure/architecture is a model of a given logical formula/property. Nowadays it is feasible to automatically generate properties for a given system model to be verified, and the correctness of model relies on the correctness of properties, how do we ensure those generated properties are both correct and complete?
EMC:
The specification of the system is the property to be checked. I am unaware of any automatic techniques for deriving the specification of a complex system. Although there are certain properties that one might want to check for certain classes of systems (e.g., absence of deadlock for concurrent programs), formulating the specification is, in general, quite hard and must be done by the person who is verifying the system. Sometimes specifications do not capture the intent of the programmer and are incorrect. Fortunately, the counterexample feature in most model checkers can help identify incorrect specifications. Also, it is very difficult to know when a specification is complete and captures all of the properties that are necessary for correct functioning of the system. Developing tools to help with system specification would be an important breakthrough.
FJ:
While after over 20 years use of BDDs various BDD-based algorithms have been developed and BDD-techniques have seen dramatic improvements since the full potential for efficient algorithms based on BDD in mid-1980s, recently SAT based techniques are reconsidered with respect to their usability in formal verification. From model checking perspective, could you offer us a fair comparison between BDD-based approach and SAT-based approach, their respective strength and weakness? Do you envision a possible novel, elegant and efficient 3rd solution for model checking?
EMC:
Ultimately, I think BDD-based techniques will give way to techniques that use fast SAT Solvers and other decision procedures. For example, there has been a lot of research during the last couple of years on bit-vector decision procedures for handling integer arithmetic in model checkers for programming languages like C. I think this trend is likely to continue.
FJ;
Verifying software is harder than verification hardware, and verifying real-time software such as embedded software is even more harder, what is your opinion on state-of-the-art of model checking for real-time software?
EMC:
If time is assumed to be discrete, then model checking is usually feasible. Often discrete time is sufficient. However, if time is assumed to be continuous, model checking is much harder. Even the most powerful real-time model checkers can only handle a relatively small number of clock variables. The same problem occurs with hybrid systems that involve both discrete and continuous behaviors¡ªonly a few continuous state variables can be handled with state-of-the-art model checkers. Since safety critical embedded systems often involve real-time constraints and hybrid behavior, this is a very important topic for research.
FJ:
What is your opinion on the importance of applying informal and semi-formal verification techniques for system verification?
EMC:
Semi-formal techniques like runtime verification and incomplete model checking using some coverage criterion are very important when the system is too large for standard model checking techniques. I am currently investigating a technique called Statistical Model Checking, which may give an incorrect answer, but the probability of getting a wrong answer can be bounded.
FJ:
In migrating from pure Research to industrial reality, how did you strike the balance between the beauty of theory and the elegance of application?
EMC:
I regard myself as a pragmatist. If a model checking technique scales to large systems and can handle the state explosion problem, then I am quite happy. I don¡¯t think a model checking technique that did not scale to large systems could ever be beautiful. Often model checking techniques are very clever and involve some deep insight into what into the source of system complexity. A recent example is Ken McMillan¡¯s use of Craig Interpolation for finding invariants.
FJ:
Verifying embedded system is harder than verifying embedded software, and verifying hybrid system surely us even harder than verifying embedded system, what is your projection of applying model checking techniques for hybrid system verification?
EMC:
I am currently working on this problem myself. I wish I knew a good answer to your question. Techniques that use numerical approximations for the solutions of differential equations are subject to error since the approximations are rarely exact. The error can actually change the truth-value of a specification and cause the model checker to be unsound. Symbolic techniques can avoid numerical error but may require closed form solutions for differential equations. This is problematic since not all differential equations have closed form solutions. Even if a closed form solutions does exist, the computer algebra needed for reasoning about the solutions may have high complexity.
FJ:
After practicing computer science and electrical engineering for over decades, what is your career advice for those who are working at the front-line of high-tech industry?
EMC:
I think that Engineers developing safety critical software should be familiar with automatic verification techniques, including both model checkers and automated proof checkers. Several model checkers (Cadence SMV, NuSMV, Spin, etc.) are easy to obtain and experiment with. Those interested in doing research in automated verification may wish to attend conferences like CAV and TACAS or at least obtain the proceedings of these conferences. I believe that formal verification is still in its infancy and that someone who wants to do research in this area will have no difficulty finding important research problems.
Back to Home Page