About the suitability of Petri nets for describing, validating and evaluating SA-RT specifications

Use of specification methodologies for Real-Time systems is highly important. Structured methodologies like SA-RT lacks formalism which makes it difficult to evaluate the resulting specifications. This paper deals with the ability of Petri nets to describe, to validate and to evaluate SA-RT specifications. A quick survey of papers studying the joint use of SA-RT and Petri nets is presented. Then, the way Petri nets are used to describe SA-RT specifications is briefly exposed. Possibilities given by Petri nets to validate specifications are investigated emphasizing on models which are suitable for real-time systems: Time Petri Nets and Stochastic Timed Petri Nets. We show that Petri nets does not give a significant benefit to SA-RT-specs validation, but they are of great interest for the consistency analysis of time and functional specifications, and for the evaluation of time properties. A small example illustrates the ability of these models to help evaluating SA-RT specifications