PROTOCOL VERIFICATION SYSTEM FOR SDL SPECIFICATIONS BASED ON ACYCLIC EXPANSION ALGORITHM AND TEMPORAL LOGIC

This paper describes a system which verifies that the behaviors of a protocol specified in SDL meet requirements. Requirements are expressed using a branching-time temporal logic for a concise and unambiguous description. The verification system first generates a set of state transition graphs consisting of executable transitions, and then evaluates the branching-time temporal logic formula on the graphs. Using an extended acyclic expansion algorithm, the state transition graph is obtained for each process, while the existing verification methods use a global state transition graph that represents the behaviors of the whole protocol system consisting of all processes. Since only the graphs of the processes relevant to the requirements are examined, the verification can be executed more efficiently. The verification is illustrated in the paper by the verification of a broadcasting protocol for requirements such as fair termination among processes.