Distributed automata in an assumption-commitment framework |
| |
Authors: | Swarup Mohalik R Ramanujam |
| |
Affiliation: | (1) Sasken Communications Technology Ltd, 560 071 Bangalore, India;(2) The Institute of Mathematical Sciences, 600 113 Taramani, Chennai, India |
| |
Abstract: | We propose a class of finite state systems of synchronizing distributed processes, where processes make assumptions at local
states about the state of other processes in the system. This constrains the global states of the system to those where assumptions
made by a process about another are compatible with the commitments offered by the other at that state. We model examples
like reliable bit transmission and sequence transmission protocols in this framework and discuss how assumption-commitment
structure facilitates compositional design of such protocols. We prove a decomposition theorem which states that every protocol
specified globally as a finite state system can be decomposed into such an assumption compatible system. We also present a
syntactic characterization of this class using top level parallel composition.
The main results here were first reported in an earlier paper (Mohalik & Ramanujam 1998). We thank the anonymous reviewers
for detailed comments that helped to improve the presentation |
| |
Keywords: | Assumption-commitment automata theory concurrency theory verification decomposition |
本文献已被 SpringerLink 等数据库收录! |