The authors present an extension to real-time structured analysis (SA-RT) for the detailed design of embedded real-time systems, and combine the proposed notation with Petri nets.

Felder and Pezzè describe their extended real-time structured analysis notation (RTD) in detail, and also describe high-level timed Petri nets, the model used to give formal semantics to RTD. A case study of the use of RTD for modeling a chemical plant controller is described. Finally, the paper illustrates verification and validation capabilities by showing how to prove safety properties in a case study, and by discussing the support provided to verify the compatibility of different design variants with the requirements specifications.