Synthesizing protocol specifications from service specifications in timed extended finite state machines

Abstract

We propose a specification model and present a method to algorithmically\nderive a protocol specification from a service specification based on\nthe model.\n\nUnlike the previous models based on finite state machines, the proposed\nmodel can explicitly express concurrency, synchronization, and timing\nrequirements such as delays and timeouts. We assume that there exists\na reliable communication channel between any two protocol entities and\nthe maximum delay for each channel is bounded by a positive constant.\nBecause of the variable nature of the communication delays along with\nthe time constraints associated with events, no protocol specification\ncan fully simulate the service specification.\nThe proposed method derives a protocol specification that is optimal\nin the sense that it provides the largest possible subset of the service\nspecification under the communication delay constraints.\nWe also give a method to derive a sub specification from a service \nspecification and a maximum communication delay of each channel such that\nthe sub specification, but no superset of it, can be simulated by the\nderived protocol specification.