1-1hit |
A protocol completion method is proposed to transform protocols synthesized from service specifications into error-free protocols. Communication service specifications described by message sequence charts can be synthesized into protocols. The synthesized protocols may include latent exceptional behaviors that are beyond the given service specifications. Therefore, even if the service specifications themselves are verified, these exceptional behaviors may produce protocol errors such as deadlock states or unspecified reception. Error-free protocols can be obtained from error-free service specifications by synthesizing and then completing the synthesized protocols. By taking account of each service specification through protocol completion, every exceptional behavior can be detected in the protocol entities including erroneous exceptional behaviors. This function can also be applied to resolution of feature interactions. The proposed method is applied to the synthesis of the X.227 protocol from its partial service specifications.