Algorithmic aspects of hierarchical verification for SA/RT models

Structured analysis methods for real-time systems (SA/RT) use highly expressive graphical specification languages to specify system requirements. By giving semantics via selected formal models to SA/RT specifications, their user-friendly and problem-oriented characteristics can be retained, whilst the existing results of formal models can be used-for easier simulation and more powerful analysis. Previous work proposed a compositional and efficient method for translating SA/RT models into high-level timed Petri nets. In this paper, we consider how to verify SA/RT models by means of the resultant Petri nets, in order to support the SA/RT hierarchical development