Automatic Verification in Formal Methods in Software Engineering

Automatic Verification in Formal Methods in Software Engineering

1. Formal Methods in SE Umer Abid 2021-SE-03 Abdullah Shahid 2021-SE-32 Lecture # 11 1

2. Automatic Verification 2

3. How can we check the model? The model is a graph. The specification should refer the graph representation. Apply graph theory algorithms. 3

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

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

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

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

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. 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

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

10. Start from an initial state 10 q 3 q 4 q 2 q 1 q 5 q 1 q 1 Stack: Hash table:

11. Continue with a successor 11 q 3 q 4 q 2 q 1 q 5 q 1 q 2 q 1 q 2 Stack: Hash table:

12. One successor of q 2 . 12 q 3 q 4 q 2 q 1 q 5 q 1 q 2 q 4 q 1 q 2 q 4 Stack: Hash table:

13. Backtrack to q 2 (no new successors for q 4 ). 13 q 3 q 4 q 2 q 1 q 5 q 1 q 2 q 4 q 1 q 2 Stack: Hash table:

14. Backtracked to q 1 14 q 3 q 4 q 2 q 1 q 5 q 1 q 2 q 4 q 1 Stack: Hash table:

15. Second successor to q 1 . 15 q 3 q 4 q 2 q 1 q 5 q 1 q 2 q 4 q 3 q 1 q 3 Stack: Hash table:

16. Backtrack again to q 1 . 16 q 3 q 4 q 2 q 1 q 5 q 1 q 2 q 4 q 3 q 1 Stack: Hash table:

17. The state graph: Successor relation between states. 17 Turn=0 L0,L1 Turn=0 L0,NC1 Turn=0 NC0,L1 Turn=0 CR0,NC1 Turn=0 NC0,NC1 Turn=0 CR0,L1 Turn=1 L0,CR1 Turn=1 NC0,CR1 Turn=1 L0,NC1 Turn=1 NC0,NC1 Turn=1 NC0,L1 Turn=1 L0,L1

18. ¬ ( PC0=CR0/\PC1=CR1) is an invariant! 18 Turn=0 L0,L1 Turn=0 L0,NC1 Turn=0 NC0,L1 Turn=0 CR0,NC1 Turn=0 NC0,NC1 Turn=0 CR0,L1 Turn=1 L0,CR1 Turn=1 NC0,CR1 Turn=1 L0,NC1 Turn=1 NC0,NC1 Turn=1 NC0,L1 Turn=1 L0,L1

19. []( Turn=0  <>Turn=1) 19 Turn=0 L0,L1 Turn=0 L0,NC1 Turn=0 NC0,L1 Turn=0 CR0,NC1 Turn=0 NC0,NC1 Turn=0 CR0,L1 Turn=1 L0,CR1 Turn=1 NC0,CR1 Turn=1 L0,NC1 Turn=1 NC0,NC1 Turn=1 NC0,L1 Turn=1 L0,L1

20. 20 Turn=0 L0,L1 Turn=0 L0,NC1 Turn=0 NC0,L1 Turn=0 CR0,NC1 Turn=0 NC0,NC1 Turn=0 CR0,L1 Turn=1 L0,CR1 Turn=1 NC0,CR1 Turn=1 L0,NC1 Turn=1 NC0,NC1 Turn=1 NC0,L1 Turn=1 L0,L1 init New initial state Convert graph into Buchi automaton

21. 21 Turn=0 L0,L1 Turn=1 L0,L1 init Propositions are attached to incoming nodes. All nodes are accepting. Turn=1 L0,L1 Turn=0 L0,L1

22. Correctness condition Correctness conditions are specific properties or requirements that a system or program must satisfy to be considered correct. These conditions can be expressed in various formalisms, such as temporal logic, modal logic, or algebraic specifications. In other words, correctness conditions are used to formally verify that a system meets its specifications. 22

23. Correctness condition We want to find a correctness condition for a model to satisfy a specification. Language of a model: L(Model) Language of a specification: L(Spec). We need: L(Model)  L(Spec). 23

24. Correctness 24 All sequences Sequences satisfying Spec Program executions

25. How to prove correctness? Show that L(Model)  L(Spec). Equivalently: ______ Show that L(Model)  L(Spec) = Ø. Also: can obtain Spec by translating from LTL! 25

26. Emptiness Emptiness: To check if an automaton is empty, we need to determine if there exists an accepting run. Accepting run: An accepting run is a sequence of states that the automaton can go through, starting from the initial state and ending in an accepting state, such that the automaton passes through an accepting state infinitely often. 26

27. Continue… An automaton is considered empty if there is no possible way for it to reach an accepting state after processing any input string. To check for emptiness, we need to find out if there's at least one path through the automaton that leads to an accepting state and can be repeated infinitely. 27

28. Emptiness... Need to check if there exists an accepting run (passes through an accepting state infinitely often). 28

29. How to check for emptiness? 29 s ,t s ,t 1 s 1 ,t 1 b a c a c

30. Strongly Connected Component (SCC) A set of vertices (or nodes) in a directed graph where there exists a path from every vertex to every other vertex within the set. In other words, it's a subgraph where any node can reach any other node within the subgraph by following the directed edges. 30

31. Strongly Connected Component (SCC) Maximality: SCCs are maximal in the sense that we can't add any more vertices to them without losing the strongly connected property. Disjointness : SCCs are disjoint, meaning that no vertex can belong to more than one SCC. 31

32. Strongly Connected Component (SCC) A set of states with a path between each pair of them . 32 Can use Tarjan’s DFS algorithm for finding maximal SCC’s.

33. Finding accepting runs If there is an accepting run, then at least one accepting state repeats on it forever. Look at a suffix of this run where all the states appear infinitely often . These states form a strongly connected component on the automaton graph, including an accepting state. Find a component like that and form an accepting cycle including the accepting state. 33

34. Equivalently... A strongly connected component: a set of nodes where each node is reachable by a path from each other node. Find a reachable strongly connected component with an accepting node. 34

35. 35 THE END