Model Checking Evolution

Explicit-State Model Checking (EMC)

• State space can be viewed as graph
• Exhaustively enumerates all states of the system and traverses each edge of the graph
• Problem
  • Huge state space and difficult to enumerate all (computer capability CPU and memory consumption)
• Depth-First Search or Breadth-First Search
  • BFS: the shortest counterexample available
  • BFS: more memory required since it needs to store back-pointers to predecessor state
• States: 10^5

Symbolic Model Checking

• Manipulate set of states and transitions, rather than individual state and transition
• Set of states and transitions is represented Boolean formula (boolean encoding)
• BDD: boolean formula as Binary Decision Diagram

Boolean function:

• describes how to determine a Boolean value output based on some logical calculation from Boolean inputs
• for a set A, each element of f(A) is called a Boolean function generated by A.
• each boolean function is a unique representation
• for example, for two binary variables (x and y), it has (2^2^(card(A)) = 16) boolean function. Here f1 = x AND y, and f2 = x OR y

  x | y | f1 | f2 | …
  0 | 0 | 0 | 0 | …
  0 | 1 | 0 | 1 | …
  1 | 0 | 0 | 1 | …
  1 | 1 | 1 | 1 | …

• Each element in the set of states is encoded as bit-string
  • for a variable vector V={v1,v2,…vn}. A bit-string can represent 2^n states. For example, if n = 3, the set of states can be {000, 001, 010, 011, 100, 101, 110, 11}. Here bit-string 000 is a representation of bits vector {v1=0,v2=0,v3=0}.
• Characteristic boolean function
  • represents a subset of states which makes the function is true.
  • for instance, if characteristic function is v1 AND v2, it means v1 and v2 should be both true. So the set will be {110,111}.
• Current state of a vector of variable is symbolised as a bit-string
• Transition is a state pair (s,s’), a combined bit-string
• States: 10^100
• SMV: Symbolic Model Verifier

Bounded Model Checking

• Bounded in user-supplied time k
• For transition system M, temporal logic formula f, construct a propositional formula Omega(k) that is satisfiable if f is valid along the path of length k
• Path of length k is expressed as: I(s0) AND R(s0,s1) AND R(s1,s2) … AND R(sk-1, sk)
• For example, if k = 2, and f = EF p, then Omega(2)=I(s0) AND R(s0,s1) AND R(s1,s2) AND (p0 OR p1 OR p2), which means from initial states, after up to 2 steps (transition), at least one p is true (exactly the same meaning as EF - exists a path finally p holds)
  • not Omega(2) = I(s0) AND R(s0,s1) AND R(s1,s2) AND (not p0 AND not p1 AND not p2) - counterexample, all p does not hold.
• For example, if k = 2, and f = AG p, then Omega(2)=I(s0) AND R(s0,s1) AND R(s1,s2) AND (p0 AND p1 AND p2), which means from initial states, after up to 2 steps (transition), each p is true (exactly the same meaning as AG - for all paths p always holds)
  • not Omega(2) = I(s0) AND R(s0,s1) AND R(s1,s2) AND (not p0 OR not p1 OR not p2) - counterexample, at least one p does not hold.
  • Safety-checking becomes not Omega(k) is not satisfiable. If it is satisfied, a satisfying assignment is given and that is the counterexample.
• Using SAT
• States: 10^1000

SAT

• given a propositional formula, find if there exists an assignment to Boolean variables that make the formula true.
  • for example, two boolean variables x and y. Formula p = not x AND not y. To make p true, A={x=0,y=0} is the only SATisfying assignment.

Pros

• SAT solvers do not require exponential space and large designs can be checked very fast. BDDs based model checking uses DFS or BFS which does require a large memory.

References

• The courses taught by Edmund M. Clarke in Carnegie Mellon University

​

[English Writing] Good references

Reference

In particular, his calculations suggest, the firn of the Wilkins, Larsen C, George VI and Cosgrove shelves in west Antarctica will be saturated with meltwater by the end of the century--a finding which echoes that of a study led by Jan van Angelen, also of Utrecht University, that was published last year in Geophysical Research Letters. [P67, The Economist (Feb 07, 2014)]

This, as they reported in December’s Nature Geoscience, contains some 140 bil- lion tonnes of liquid water. [P67, The Economist (Feb 07, 2014)]

Further explanation or description

Parenthesis

There is, for example, little Neanderthal DNA on the X chromosome (which, along with the Y chromosome, determines an individual’s sex). [P66, The Economist (Feb 07, 2014)]

Dr Forster and his colleagues think the aquifer they have found covers an area of 70,000 square kilometres (about the size of Ireland). [P67, The Economist (Feb 07, 2014)]

em dash (--)

For instance, genes affecting the production of keratin--an important component of hair and skin--showed more Neanderthal influence than most. [P66, The Economist (Feb 07, 2014)]

This would not matter as a one-off, but if it happened repeatedly as new firn formed the consequences could be serious--particularly if, in escaping, it caused more hydrofracturing or acted as a lubricant that encouraged previously stable ice to slip from its bed- rock into the sea. [P67, The Economist (Feb 07, 2014)]

How likely that sort of thing is to happen--and thus how much of a threat firn really is--has yet to be determined. [P67, The Economist (Feb 07, 2014)]

Enumerate

And two studies, one just published in Nature, and one in Science, have now looked in detail at this miscegenation, and tried to understand its consequences. [P66, The Economist (Feb 07, 2014)]

Emphasise

But the fact that so little is known about it emphasises a wider point. [P67, The Economist (Feb 07, 2014)]

Misc

Crucially, though the amount of Neanderthal DNA in any individual is small, the exact bits vary a lot from person to person. [P67, The Economist (Feb 07, 2014)]

Technically, Neanderthals may be gone. But their DNA ghosts linger on. [P67, The Economist (Feb 07, 2014)]

SVN "local unversioned, incoming add upon update"

Problem

$ svn st -q
D     C dir
      >   local unversioned, incoming add upon update
D       dir/file

Solution

$ svn resolve --accept working dir
Resolved conflicted state of 'dir'
$ svn revert dir
Reverted 'dir'
$ svn status
D       dir/file
$ svn revert dir/file
Reverted 'dir/file'
$ svn st -q 

Reference

• http://tomhennigan.blogspot.co.uk/2012/01/resolve-tree-conflict-svn-local.html