P Chandrasekaran and M Mukund
Next Generation Design and Verification Methodologies
for Distributed Embedded Control Systems
S Ramesh and P Sampath (eds.),
Springer (2007) 83-97.
Message Sequence Charts (MSCs) are used to specify the behaviour of communicating systems through scenarios. Though timing constraints are natural for describing the behaviour of real-life protocols, the basic MSC notation has no mechanism to specify such constraints. We propose a notation for specifying collections of timed scenarios and describe a framework for automatic verification of scenario-based properties for communicating finite-state machines equipped with local clocks.