In: Lecture Notes in Computer Science : Formal Techniques for Networked and Distributed Systems - FORTE 2006, Volume 4229, 2006, pages 388-403. 2006. URL: http://dx.doi.org/10.1007/1188811628.
Abstract: 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.