tailieunhanh - Lecture Formal methods in software engineering: Automatic verification

In this chapter, the following content will be discussed: How can we check the model? What properties can we check? How to perform the checking? If it is so good, why learn deductive verification methods? If it is so constrained, is it of any use? Depth first search, start from an initial state, how can we check properties with DFS?. | 1 Formal Methods in SE Qaisar Javaid Assistant Professor Lecture # 11 2 Automatic Verification 3 How can we check the model? The model is a graph. The specification should refer the the graph representation. Apply graph theory algorithms. 3 9 4 What properties can we check? Invariant: a property that needs to hold in each state. Deadlock detection: can we reach a state where the program is blocked? Dead code: does the program have parts that are never executed. 4 10 5 How to perform the checking? Apply a search strategy (Depth first search, Breadth first search). Check states/transitions during the search. If property does not hold, report counter example! 5 11 6 If it is so good, why learn deductive verification methods? Model checking works only for finite state systems. Would not work with Unconstrained integers. Unbounded message queues. General data structures: queues trees stacks parametric algorithms and systems. 6 12 7 The state space explosion Need to represent the state space of a program in the computer memory. Each state can be as big as the entire memory! Many states: Each integer variable has 2^32 possibilities. Two such variables have 2^64 possibilities. In concurrent protocols, the number of states usually grows exponentially with the number of processes. 7 13 8 If it is so constrained, is it of any use? Many protocols are finite state. Many programs or procedure are finite state in nature. Can use abstraction techniques. Sometimes it is possible to decompose a program, and prove part of it by model checking and part by theorem proving. Many techniques to reduce the state space explosion. 8 14 9 Depth First Search Program DFS For each s such that Init(s) dfs(s) end DFS Procedure dfs(s) for each s’ such that R(s,s’) do If new(s’) then dfs(s’) end dfs. 9 15 10 Start from an initial state q3 q4 q2 q1 q5 q1 q1 Stack: Hash table: 10 16 11 Continue with a successor q3 q4 q2 q1 q5 q1 q2 q1 q2 Stack: Hash table: 11 17 12 One successor of q2. q3 q4 q2 q1 . | 1 Formal Methods in SE Qaisar Javaid Assistant Professor Lecture # 11 2 Automatic Verification 3 How can we check the model? The model is a graph. The specification should refer the the graph representation. Apply graph theory algorithms. 3 9 4 What properties can we check? Invariant: a property that needs to hold in each state. Deadlock detection: can we reach a state where the program is blocked? Dead code: does the program have parts that are never executed. 4 10 5 How to perform the checking? Apply a search strategy (Depth first search, Breadth first search). Check states/transitions during the search. If property does not hold, report counter example! 5 11 6 If it is so good, why learn deductive verification methods? Model checking works only for finite state systems. Would not work with Unconstrained integers. Unbounded message queues. General data structures: queues trees stacks parametric algorithms and systems. 6 12 7 The state space explosion Need to represent the state .