Title :
Automated synthesis of protocol specifications with message collisions and verification of timeliness
Author :
Kakuda, Yoshiaki ; Igarashi, Hirotaka ; Kikuno, Tohru
Author_Institution :
Dept. of Inf. & Comput. Sci., Osaka Univ., Japan
Abstract :
Protocol synthesis is used to derive a protocol specification based on a service specification. In the previous protocol synthesis methods, if the service specification includes simultaneous transmission of primitives, then the derived protocol specification includes protocol errors of unspecified receptions caused by message collisions. This paper extends a class of derived protocol specifications to include message collisions which often happen in real communication protocols, and proposes a protocol synthesis method such that (1) simultaneous transmission of primitives causing message collisions can be described in the service specifications, and (2) transitions for avoiding protocol errors of unspecified receptions can be generated by new transition synthesis rates. This paper also proposes a verification method for determining a real-time bound in the synthesized protocol specification using the task scheduling algorithm for multiprocessor systems
Keywords :
communicating sequential processes; finite state machines; message switching; multiprocessing systems; processor scheduling; protocols; telecommunication computing; telecommunication services; automated synthesis; communication protocols; finite state machines; message collisions; message verification; multiprocessor systems; protocol errors; protocol specifications; protocol synthesis; real-time bound; sequences; service specification; simultaneous primitives transmission; task scheduling algorithm; transition synthesis rates; Access protocols; Electronic mail; Intelligent networks; Multiprocessing systems; Network synthesis; Polynomials; Rail transportation; Real time systems;
Conference_Titel :
Network Protocols, 1994. Proceedings., 1994 International Conference on
Conference_Location :
Boston, MA
Print_ISBN :
0-8186-6685-4
DOI :
10.1109/ICNP.1994.344366
