Patent ID: 6466646
Filing Date: 2002-10-15
Classification: G06F,H04M

Abstract:
Method of verifying the operation of a system modeled by a system of automata synchronised by a set of messages, including the following operations:breaking down the system into N subsystems numbered from n=1 to n=N; providing parameters describing each subsystem n (1&lE;n&lE;N) in the form of a respective automaton composed of a set En of states eni of the subsystem n with a set An of transitions ani between pairs of states of the set En, each transition anj of the set An being associated with a subset Mnj of the set of synchronisation messages to translate the fact that each message of the subset Mnj arises when the subsystem described changes state in accordance with the transition anj; constructing a system of linear equations including, for 1&lE;t&lE;T and 1&lE;n&lE;N, on the one hand flow equations of the form: eni&it;â€ƒ&it;(t-1)=&Sum;j&Element;Bni&it;â€ƒ&it;anj&it;â€ƒ&it;(t)&it;â€ƒ&it;for&it;â€ƒ&it;eni&Element;Enand of the form: eni&it;â€ƒ&it;(t)=&Sum;j&Element;Cni&it;â€ƒ&it;anj&it;â€ƒ&it;(t)&it;â€ƒ&it;for&it;â€ƒ&it;eni&Element;En,and on the other hand synchronization equations of the form: mk&it;â€ƒ&it;(t)=&Sum;j&Element;Dnk&it;â€ƒ&it;an&it;â€ƒ&it;(t)&it;â€ƒ&it;for&it;â€ƒ&it;mk&Element;Mn,where T designates a number of successive steps of the operation of the system, Bni designates the set of the indices j such that the transition anj the set An, starts from the state eni of the set En, Cnj designates the set of the indices j such that the transition ani of the set An, leads to the state eni of the set En, Mn designates the union of the subsets of messages Mnj respectively associated with the transitions of the set An, Dnk designates the set of the indices j such that a message mk of the set Mn belongs to the subset Mnj associated with the transition anj of the set An, the variable eni(t) (0&lE;t&lE;T) is an unknown of the linear system associated with the state eni of the set En and with step t, the variable anj(t) (1&lE;t&lE;T) is an unknown of the linear system associated with the transition anj of the set An and with step t, the variable mk(t) (1&lE;t&lE;T) is an unknown of the linear system associated with the message mk of set of synchronisation messages and with step t;defining a property of the system to be verified in the form of additional linear constraints imposed on the unknowns of the linear system; applying a linear programming solution method to the linear system subject to the additional constraints; analysing the result of linear programming to determine if said property is verified by the system; and assisting a user to detect malfunction of said system or to obtain evidence of correct operation of said system or to obtain evidence of correct operation of said system.