Madhavan Mukund

Adding time to scenarios

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.

  • Download PDF.