Synthesizing Protocol Specifications from Service Specifications in Timed Extended Finite State Machines

dc.contributor.authorPark, Jun-Cheolen_US
dc.contributor.authorMiller, Raymond E.en_US
dc.description.abstractWe propose a specification model and present a method to algorithmically derive a protocol specification from a service specification based on the model. Unlike the previous models based on finite state machines, the proposed model can explicitly express concurrency, synchronization, and timing requirements such as delays and timeouts. We assume that there exists a reliable communication channel between any two protocol entities and the maximum delay for each channel is bounded by a positive constant. Because of the variable nature of the communication delays along with the time constraints associated with events, no protocol specification can fully simulate the service specification. The proposed method derives a protocol specification that is optimal in the sense that it provides the largest possible subset of the service specification under the communication delay constraints. We also give a method to derive a sub specification from a service specification and a maximum communication delay of each channel such that the sub specification, but no superset of it, can be simulated by the derived protocol specification.en_US
dc.format.extent289322 bytes
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.relation.isAvailableAtTech Reports in Computer Science and Engineeringen_US
dc.relation.isAvailableAtComputer Science Department Technical Reportsen_US
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3693en_US
dc.titleSynthesizing Protocol Specifications from Service Specifications in Timed Extended Finite State Machinesen_US
dc.typeTechnical Reporten_US


Original bundle
Now showing 1 - 2 of 2
No Thumbnail Available
282.54 KB
Postscript Files
Thumbnail Image
218.83 KB
Adobe Portable Document Format
Auto-generated copy of