Verification of Scenario-based Specifications using Templates

Specifying dynamic behaviour of a system by listing scenarios of its interactions has become a popular practice. Message sequence chart (MSC) is a rigorous and widely used notation for specifying such scenarios of system behaviour. High-level MSCs (HMSC) provide hierarchical and modular composition facilities for constructing complex scenarios from basic MSCs. Although the general problem of formal verification of properties of HMSCs is intractable, we propose a framework for restricted verification. We present simple templates for commonly used types of properties and discuss efficient algorithms for verifying them.