Checking MSC specifications for timing inconsistency

Message sequence chart (MSC) is a graphical and textual language for the description and specification of the interactions between system components. MSC specifications allow convenient expression of multiple scenarios, and offer an intuitive and visual way of describing design requirements. Like any other aspect of the specification and design process, MSCs are amenable to errors, and their analysis is important. In this paper, the verification problem of MSC specification for timing inconsistency is studied, which means that no execution scenario described by an MSC specification is timing consistent. An algorithm is developed to check MSC specifications for timing inconsistency.