|
Scenario languages based on Message Sequence Charts (MSCs) have been widely
studied in the last decade. The high expressive power of MSCs renders many basic
problems concerning these languages undecidable. However, several of these problems are
decidable for languages that possess a behavioral property called "existentially bounded".
Unfortunately, collections of scenarios outside this class are frequently exhibited by
systems such as sliding window protocols. We propose here an extension of MSCs called
causal Message Sequence Charts and a natural mechanism for defining languages of causal
MSCs called causal HMSCs (CaHMSCs). These languages preserve decidable properties
without requiring existential bounds. Further, they can model collections of scenarios
generated by sliding window protocols. We establish here the basic theory of CaHMSCs as
well as the expressive power and complexity of decision procedures for various subclasses
of CaHMSCs. We also illustrate the modeling power of our formalism with the help of a
realistic example based on the TCP sliding window feature
[.pdf]
|