Protocol validation system

Claim 2

A protocol validation system for a design procedure for software in a communication system, receiving a protocol specification in a form of electrical signals, and testing said protocol specification through a transition of global states according to transition information of said protocol specification, to find an error of said protocol specification, said system comprising: (a) a memory for storing a set of said protocol specification which is subject to validation, (b) means for deriving the initial global state, which is composed of initial states of all the processes in said specification and signal series in signal reception buffers between said processes, based on said specification stored in said memory, (c) means for registering a global state as a member of a set of yet to be processed global states, (d) means for selecting one member from said set of yet to be processed global states, (e) means for obtaining global transition candidates, each of which is a combination of immediately executable transitions at said member global state of said set of yet to be processed global states, (f) means for determining nonredundant global transitions at said global state by deleting redundant global transitions from said global transition candidates according to a predetermined condition, (g) means for registering every process transition in said nonredundant global transitions as a member of a set of executable process transitions, (h) means for deriving global states, which are composed of the state of all the processes in said protocol specification and signal series in signal reception buffers between said processes, by the execution of said nonredundant global transitions, (i) means for detecting errors by investigating said global states in comparison with said protocol specification, (j) means for registering each of said global states, which has yet to be processed by means (d) through (h), as a member of said set of yet to be processed global states, (k) means for detecting errors by comparing the members of said set of executed process transitions with said protocol specification.

Claim 3

A protocol validation system for a design procedure for software in a communication system, receiving a protocol specification in a form of electrical signals, and testing said protocol specification through a transition of global states according to transition information of said protocol specifications, to find an error of said protocol specification, said system comprising: (a) a memory for storing a set of said protocol specification which is subject to validation, (b) means for deriving the initial global state, which is composed of initial states of all the processes in said specification and signal series in signal reception buffers between said processes, based on said specification stored in said memory, (c) means for registering a global state as a member of a set of yet to be processed global states, (d) means for selecting one member from said set of yet to be processed global states, (e) means for obtaining global transition candidates, each of which is combination of immediately executable transitions at said member global state of said set of yet to be processed global states, (f) means for determining nonredundant global transitions at said global state by deleting redundant global transitions from said global transition candidates according to a predetermined condition, (g) means for registering every process transition in said nonredundant global transitions as a member of a set of executable process transitions, (h) means for deriving global states, which is composed of the state of all the processes in said protocol specification and signal series in signal reception buffers between said processes, by the execution of said nonredundant gobal transitions, (i) means for detecting errors of deadlocks by investigating whether there exists no immediately executable and specified process transition at said global state and for detecting errors of unspecified reception by investigating whether there exists any immediately executable but not specified reception at said global state, (j) means for registering each of said global states, which has yet to be processed by means (d) through (h), as a member of said set of yet to be processed global states, (k) means for detecting errors of redundant reception by investigating whether there exists any specified transition which is not equal to any member of said set of executed process transitions.

Claim 4

A protocol validation system for a design procedure for software in a communication system, receiving a protocol specification in a form of electrical signals, and testing said protocol specification through a transition of global states according to transition information of said protocol specifications, to find an error of said protocol specification, said system comprising: (a) a memory for storing a set of said protocol specification which is subject to validation, (b) means for deriving the initial global state, which is composed of initial states of all the processes in said specification and signal series in signal reception buffers between said processes, based on said specification stored in said memory, (c) means for registering a global state as a member of a set of yet to be processed global states, (d) means for selecting one member from said set of yet to be processed global states, (e) means for obtaining global transition candidates, each of which is combination of immediately executable transitions at said member global state of said set of yet to be processed global states, (f) means for determining nonredundant global transitions at said global state by deleting redundant global transitions from said global transition candidates according to a predetermined condition, (g) means for registering every process transition in said nonredundant global transitions as a member of a set of executable process transitions, (h) means for deriving global states, which is composed of the state of all the processes in said protocol specification and signal series in signal reception buffers between said processes, by the execution of said nonredundant gobal transitions, (i) means for detecting errors of deadlocks by investigating whether there exists no immediately executable and specified process transition at said global state and for detecting errors of unspecified reception by investigating whether there exists any immediately executable but not specified reception at said global state, (j) means for registering each of said global states, which has yet to be processed by means (d) through (h), as a member of said set of yet to be processed global states, (k) means for detecting errors of redundant reception by investigating whether there exists any specified transition which is not equal to any member of said set of executed process transitions.