Method of verification of a finite state sequential machine and resulting information support and verification tool

Claim 3

The method according to claim 1, further comprising computing an equivalence relation E of a finite state machine (FSM), the equivalence relation E being defined as the fixpoint of a monotonic suite E 1 , . . . , E n =E, the computation of the equivalence relation E being made by successively constructing the set E n by use of the reverse image of the set E n-1 defined in terms of said set Y and corresponding to Δ -1 (E n-1 ).

Claim 4

The method according to claim 1, characterized in that said step (a) is computed from a compatible projection in which the following definition is used: let B and C be two sets and ψ a relation from B into C and let < be a total strict order on C, then the cross-section of ψ is the partial function C(ψ) defined as: ##EQU5##

Claim 5

The method according to claim 1, characterized in that said step (a) is computed from a compatible projection in which the following definition is used: let B and C be two sets and ψ a relation from B into C and let ≦ be a total order on C, then the cross-section of ψ is the partial function C (ψ) defined as: ##EQU6## and the order is selected to be a successive increasing order.

Claim 6

The method according to claim 1, characterized in that in the step (b), the vector δ* is built from the vector δ and the graph C(A), said graph being encoded on a variable s=s 1 , . . . ,s n for the domain and on a variable s'=s' 1 , . . . s' n for the codomain, and δ* is also built by using the sets D j =∃s'((s j s' j ) C(A) and performing a reverse image computation uniquely for the sets Dj.

Claim 7

The method according to claim 2, characterized in that said step (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C(E n-1 )oδ.

Claim 8

The method according to claim 6, characterized in that it further comprises a step (c) of computing equivalent pairs of states with respect to the vector δ n-1 to have the pairs of (∀xΔ -1 (E n-1 )).

Claim 9

A computer implemented method of verification of a finite state sequential machine, comprising: computing by means of a data processor a set Y defined from two finite sets B and S encoded on boolean variables, a function δ:B→S expressed by a vector of boolean functions, and an equivalence relation A on S, the set B being encoded on variables s=s 1 , . . . , s n and x=x 1 , . . . , x k , in which x can be void, and Qx i designating either ∃x i or ∀x i , so that: Y={(s,s') ε(∃x 1 , . . . , ∃x k B) 2 |Qx 1 , . . . , Qx k ((δ(s,x),δ(s',x))εA)}, characterized in that the: computation of set Y comprises the steps of: (a) constructing in a canonical way, from a binary decision diagram (BDD) of a graph of the equivalence relation A, the BDD of a graph of a total function from S×S, named cross-section and denoted C(A); (b) constructing from the cross-section C(A) and the vector δ a new vector denoted δ'=C(A)oδ: and (c) computing the pairs (s,s') such that Qx1, . . . Qxk . (δ*(s,x)=δ(s',x); and verifying with said data processor an operation of said finite state sequential machine based on an equivalence relation of the pairs (s,s').

Claim 10

A computer implemented method of verification of a finite state sequential machine, comprising: computing by means of a data processor a set Y defined from two finite sets B and S encoded on boolean variables, a function δ:B→S expressed by a vector of boolean functions, and an equivalence relation A on S, the set B being encoded on variables s=s 1 , . . . , s n and x=x 1 , . . . , x k , in which x can be void, and Qx i designating either ∃x i or ∀x i , so that: Y={(s,s') ε(∃x 1 , . . . , ∃x k B) 2 |Qx 1 , . . . , Qx k ((δ(s,x),δ(s',x))εA)}, characterized in that the: computation of set Y comprises the steps of: (a) constructing in a canonical way, from a binary decision diagram (BDD) of a graph of the equivalence relation A, the BDD of a graph of a total function from S×S, named cross-section and denoted C(A); (b) constructing from the cross-section C(A) and the vector δ a new vector denoted δ'=C(A)oδ: and (c) computing the pairs (s,s') such that Qx1, . . . Qxk . (δ*(s,x)=δ(s',x); and verifying with said data processor an operation of said finite state sequential machine based on an equivalence relation of the pairs (s,s').

Claim 11

A tool for verification of a finite state sequential machine, characterized in that it carries out a method of verification of the finite state sequential machine, comprising: determining a set Y using a data processor, said set Y being defined from two finite sets B and S encoded on boolean variables, a function δ:B→S expressed by a vector of boolean functions, and an equivalence relation A on S, the set B being encoded on variables s=s 1 , . . . ,s n and x=x 1 , . . . ,x k , in which x can be void and Qx i designating either ∃x i or ∀x i , so that: Y={(s,s')ε(∃x 1 , . . . , ∃x k B) 2 |Qx 1 , . . . , Qx k (δ(s,x),δ(s',x)) εA)}, characterized in that the computation of set Y comprises the steps of: (a) constructing in a canonical way, from a binary decision diagram (BDD) of a graph of the equivalence relation A, the BDD of a graph of a total function from S×S, named cross-section and denoted C(A); (b) constructing from the cross-section C(A) and the vector δ a new vector denoted δ*=C(A)oδ; and (c) computing the pairs (s,s') such that Qx1, . . . Qxk .(δ*(s,x)=δ(s',x)); and verifying with said data processor an operation of said finite state sequential machine based on an equivalence relation of the pairs (s,s').

Claim 12

A tool for verification of a finite state sequential machine, characterized in that it carries out a method of verification of the finite state sequential machine, comprising: determining a set Y using a data processor, said set Y being defined from two finite sets B and S encoded on boolean variables, a function δ:B→S expressed by a vector of boolean functions, and an equivalence relation A on S, the set B being encoded on variables s=s 1 , . . . ,s n and x=x 1 , . . . ,x k , in which x can be void and Qx i designating either ∃x i or ∀x i , so that: Y={(s,s')ε(∃x 1 , . . . , ∃x k B) 2 |Qx 1 , . . . , Qx k (δ(s,x),δ(s',x)) εA)}, characterized in that the computation of set Y comprises the steps of: (a) constructing in a canonical way, from a binary decision diagram (BDD) of a graph of the equivalence relation A, the BDD of a graph of a total function from S×S, named cross-section and denoted C(A); (b) constructing from the cross-section C(A) and the vector δ a new vector denoted δ*=C(A)oδ; and (c) computing the pairs (s,s') such that Qx1, . . . Qxk .(δ*(s,x)=δ(s',x)); and verifying with said data processor an operation of said finite state sequential machine based on an equivalence relation of the pairs (s,s').

Claim 13

The method according to claim 2, characterized in that said step (a) is computed from a compatible projection in which the following definition is used: let B and C be two sets and ψ a relation from B into C and let < be a total strict order on C, then the cross-section of ψ is the partial function C(ψ) defined as: ##EQU7##

Claim 14

The method according to claim 2, characterized in that said step (a) is computed from a compatible projection in which the following definition is used: let B and C be two sets and ψ a relation from B into C and let ≦ be a total order on C, then the cross-section of ψ is the partial function C(ψ) defined as: ##EQU8## and the order is selected to be a successive increasing order.

Claim 16

The method according to claim 3, characterized in that said step (b), the vector δ* is built from the vector δ and the graph C(A), said graph being encoded on a variable s=s 1 , . . . , s n for the domain and on a variable s'=s' 1 , . . . , s n for the codomain, and δ* is also built by using the sets D j =∃s'((s j s' j )C(A) and performing a reverse image computation uniquely for the sets Dj.

Claim 17

The method according to claim 4, characterized in that said step (b), the vector δ* is built from the vector δ and the graph C(A), said graph being encoded on a variable s=s 1 , . . . , s n for the domain and on a variable s'=s' 1 , . . . , s' n for the codomain, and δ* is also built by using the sets D j =∃s'((s j s' j )C(A) and performing a reverse image computation uniquely for the sets Dj.

Claim 18

The method according to claim 5, characterized in that said step (b), the vector δ* is built from the vector δ and the graph C(A), said graph being encoded on a variable s=s 1 , . . . ,s n for the domain and on a variable s'=s' 1 , . . . , s' n for the codomain, and δ* is also built by using the sets D j =∃s'((s j =s' j )C(A) and performing a reverse image computation uniquely for the sets Dj.

Claim 19

The method according to claim 3, characterized in that said step (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C (E n-1 )oδ.

Claim 20

The method according to claim 4, characterized in that said step (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C(E n-1 )oδ.

Claim 21

The method according to claim 5, characterized in that said step (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C(E n-1 )oδ.

Claim 22

The method of claim 16, characterized in that said step, (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C(E n-1 )oδ.

Claim 23

The method of claim 17, characterized in that said step (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C(E n-1 )oδ.

Claim 24

The method of claim 18, characterized in that said step (b) comprises constructing from said cross-section and said vector δ a new vector δ n-1 =C(E n-1 )oδ.