2013 20th Asia-Pacific Software Engineering Conference (APSEC) (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.
Adel Benzina, Mario Paludetto, Jerôme Delatour, "About the Suitability of Petri Nets for Describing, Validating and Evaluating SA-RT Specifications", 2013 20th Asia-Pacific Software Engineering Conference (APSEC), vol. 00, no. , pp. 249, 1997, doi:10.1109/APSEC.1997.640182