摘要: 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 p... 展开 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. 收起