Proceedings of Joint 4th International Computer Science Conference and 4th Asia Pacific Software Engineering Conference (1997)
Clear Water Bay, HONG KONG
Dec. 2, 1997 to Dec. 5, 1997
Adel Benzina , LAAS-CNRS
Mario Paludetto , LAAS-CNRS
Jerôme Delatour , LAAS-CNRS
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.
A. Benzina, M. Paludetto and J. Delatour, "About the Suitability of Petri Nets for Describing, Validating and Evaluating SA-RT Specifications," Proceedings of Joint 4th International Computer Science Conference and 4th Asia Pacific Software Engineering Conference(APSEC), Clear Water Bay, HONG KONG, 1997, pp. 249.