In: Proc. Asia-Pacific Software Engineering Conf. and Int. Computer Science Conf., 2-5 December 1997, Hong Kong, pages 249-258. 1997. ISBN 0-8186-8271-X, IEEE CS No. PR08271, IEEE Catalog No. 97TB100207.
Abstract: Use of specification methodologies for real-time systems is highly important. Structured methodologies like SA-RT lack 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. It is shown that Petri nets do not provide significant benefit to SA-RT specification 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.
Keywords: SA-RT, formal specifications, real-time systems, specification validation, stochastic Petri nets, time Petri nets.