In this paper, we solve the consistency checking problems of concurrent and real-time system designs modelled by time Petri
nets for the scenario-based specifications expressed by message sequence charts (MSCs). The algorithm we present can be used
to check if a time Petri net satisfies a specification expressed by a given MSC which requires that if a scenario described
by the MSC occurs during the run of the time Petri net, the timing constraints enforced to the MSC must be satisfied.
Supported by the National Natural Science Foundation of China (No.60425204, No.60233020), the National Grand Fundamental Research
973 Program of China (No.2002CB312001), and by the Jiangsu Province Research Foundation (No.BK2004080).