Capturing synchronization specifications for sequential compositions

We explore the problem of adding synchronization information to high-level system specifications. At this level of specification the components of a system may follow non-trivial, but implicitly specified sequential protocol in order to perform their operations. We illustrate a method of extracting protocols for closely coupled systems of such components. A language is defined for specifying external timing and behavior. Although limited in its expressiveness, this language allows us to derive partial synchronization conditions in the form of timing inequalities. The solution to a system of timing inequalities is itself a timing expression, from which a controlling state-machine can be synthesized