Background Review
4.6 Verification Algorithms
4.6.1 First stage: Two approaches for candidate search
At first stage, two approaches including the early-terminated and the optimal methods are proposed. We will discuss in the following sections.
4.6.1.1 The early-terminated approach
The first approach is the early-terminated traverse method. Before introducing early-terminated traverse algorithm, we first consider Lemma 4.1.
Lemma 4.1 Let Ttree be a reachability tree which is bounded by upper height-bound Hup and m1 be any one of the candidate markings in Ttree. For any other candidate marking m2 in the successor path of marking m1, m2 is in the solution marking set S3 if and only if m1 is in S3.
Proof: Let etf set be the earliest task-finished set of a given schedule and transition sequence σ1 be a firing sequence that leads m1 ∈ S2 from root marking mr of Ttree to be a candidate marking, that is mr
σ1
→ m1. Assuming there exists another candidate marking m2 ∈ S3, m2 6= m1, with firing sequence σ2 that leads m2 from root marking mr of Ttree to be a candidate marking, that is mr
σ2
→ m2, and is in the successor path of marking m1.
As defined in Definition 1, it must be satisfied that etf set ⊆ σ1and etf set ⊆ σ2 where the elements of σ1 and σ2 are all in {nop} ∪ {etf set}. As described in assumption, m2 is in the successor path of marking m1, it is still satisfied that
m2
m4 m1
m
m3 m5
c
c
m6 m7 m8 m9
c
m10 root
Figure 4.6: The traverse order of early-terminated approach
σ2 = σ1∪ {nop}. This implies m2 is in solution marking set S3 if and only if m1
is in S3.
The early-terminated approach tries to minimize the size of candidate set S2 from reachable set S1. When an enqueued unvisited marking is candidate, the early-terminated algorithm ignores the candidate marking and marks it as a visited node. Then, it proceeds other unvisited nodes in queue Q until all the markings have been visited. In Figure. 4.6, as an example, the traverse order of the early-terminated approach is m, m1, m2, m3, . . . , m10. The pseudo-code of the earliest-terminated traverse method is shown in Figure. 4.7. In lines 12 to 14, it ignores the candidate marking and proceeds other unvisited nodes.
4.6.1.2 The optimal approach
The second approach to verify a schedule is the optimal approach which is im-proved from the early-terminated approach. In order to reduce reachable marking set S1, it tries to merge the redundant nodes when it proceeds Breadth-First tra-verse.
Let m be an unvisited node to be processed. If m is a candidate marking, it ignores this node by using Lemma 4.1 and proceeds other unvisited nodes in
1: procedure bfs build tree early terminated(m0)
2: Initialize Queue structure Q
3: Allocate new node nn ⊲ initialize root node
4: nn.visited ← f alse
5: nn.marking ← m0
6: nn.height ← 0
7: nn.candidate ← is candidate(nn)
8: Q.enqueue(nn)
9:
10: for all unvisited node n ∈ Q do
11: n.visit ← true
12: if n.candidate = true then
13: continue to the next node ⊲ Lemma 4.1
14: end if
15: if n.height 6 H then
16: ebl set ← find enabled trans(n.marking)
17: for all transition tr ∈ ebl set do
18: m ← n.marking
19: κ ← make firing vector from(tr)
20: m′ ← m + [A] · κ ⊲ Eq.2.8
21: Allocate new node nn
22: nn.marking ← m′
23: nn.visited ← f alse
24: nn.height ← n.height + 1
25: nn.candidate ← is candidate(nn)
26: create branch(n, nn)
27: Q.enqueue(nn)
28: end for
29: end if
30: end for
31: end procedure
Figure 4.7: The early-terminated approach
queue. If m is not a candidate marking, it finds enabled set of transitions and creates new node on each enabled transition. For each new produced node with marking m′, if there exists another node in the reachability tree, and has the same marking associated with it, then the node with marking m′ is a duplicate node. Since, the marking m′ has appeared in the tree, this new produced node is redundant. Then, it merges this redundant node to the existential node and creates transition link from marking m to the existential node. As an example in Figure. 4.8, when it proceeds marking m5, it founds the new created node with marking m7 is a duplicate node. It merges these nodes and creates transition from m5 to m7. Then, the algorithm continually proceeds other unvisited nodes in queue.
Figure 4.8: Merge the redundant nodes in optimal approach
The pseudo-code of the optimal approach is shown in Figure. 4.9. In lines 12 to 14, if the node n is a candidate marking, then it ignores this node by using Lemma 4.1 and proceeds the other nodes in queue Q. In lines 26 to 32, function f ind dual node checks whether the new created node nn is duplicate. If there exists a duplicate node, it ether returns the dual node to dual node or returns null. It continually proceeds other unvisited nodes until all nodes are visited.
1: procedure bfs build tree optimal(m0)
2: Initialize Queue structure Q
3: Allocate new node nn ⊲ initialize root node
4: nn.visited ← f alse
5: nn.marking ← m0
6: nn.height ← 0
7: nn.candidate ← is candidate(nn)
8: Q.enqueue(nn)
9:
10: for all unvisited node n ∈ Q do
11: n.visit ← true
12: if n.candidate = true then
13: continue to the next node ⊲ Lemma 4.1
14: end if
15: if n.height 6 H then ⊲ max. height H
16: ebl set ← find enabled trans(n.marking)
17: for all transition tr ∈ ebl set do
18: m ← n.marking
19: κ ← make firing vector from(tr)
20: m′ ← m + [A] · κ ⊲ Eq.2.8
21: Allocate new node nn
22: nn.marking ← m′
23: nn.visited ← f alse
24: nn.height ← n.height + 1
25: nn.candidate ← is candidate(nn)
26: dual node ← find dual node(nn)
27: if dual node 6= null then
28: create branch(n, dual node)
29: else
30: create branch(n, nn)
31: Q.enqueue(nn)
Figure 4.9: The optimal traverse approach
4.6.2 Second stage: The model-checking approach
At the second stage, we verify the given DUV schedule on all candidate markings aided by using SMV model checker. The inputs to the model checker are a FSM and a set of system specification that needs to be verified. FSM of the DUV is au-tomatically generated by the verification flow. Each candidate marking obtained from the first stage can be seen a restructured FSFG. System specification, CTL formulas, to the DUV is generated from each restructured FSFG.
Schedule S can be converted into a Moore machine. A Moore machine is defined as a 6-tuple M(W, Σ, ∆, δ, λ, w0), where W , Σ and ∆ are the finite set of state, input signal and output signal with respect. Transition function δ : W × Σ → W is a mapping function from state and an input to the next state.
Output function λ : W → ∆ is a mapping function from each state to the output signal. And, w0 is an initial state. Figure. 4.10 is an DUV schedule of a third-order IIR filter. The length of schedule S is le(S) = 6, and it can be seen as a FSM with le(S) + 1 states, where s0 is the initial state. Each state of the FSM is actually represented as a control step in S. For each task opji in S, there is an enabled signal op i j on it to indicate whether opji is enabled in each control step of S. For example, task op16 is scheduled at step 1 to step 2, and let op i j be its enabled signal. The behavioral description of FSM for task op61 is described at the bottom in Figure. 4.10.