Scenario-based specifications such as message sequence charts (MSCs) offer an intuitive and visual way of describing design
requirements. As one powerful formalism, Petri nets can model concurrency constraints in a natural way, and are often used
in modelling system specifications and designs. Since there are gaps between MSC models and Petri net models, keeping consistency
between these two kinds of models is important for the success of software development. In this paper, we use Petri nets to
model concurrent systems, and consider the problem of checking Petri nets for scenario-based specifications expressed by message
sequence charts. We develop the algorithms to solve the following two verification problems: the existential consistency checking
problem, which means that a scenario described by a given MSC must happen during a Petri net runs, or any forbidden scenario
described by a given MSC never happens during a Petri net run; and the mandatory consistency checking problem, which means
that if a reference scenario described by the given MSCs occurs during a Petri net run, it must adhere to a scenario described
by the other given MSC.
Supported by the National Natural Science Foundation of China (No.60425204, No.60233020, and No.60273036), the National Grand
Fundamental Research 973 Program of China (No.2002CB312001), and by Jiangsu Province Research Foundation (No.BK2004080, No.BK2003408)