Algorithmic aspects of hierarchical verification for SA/RT models

Author

Shi, Lihua ; Keane, John A.

Author_Institution

Dept. of Comput., Manchester Metropolitan Univ., UK

Volume

3

fYear

1997

fDate

12-15 Oct 1997

Firstpage

2252

Abstract

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

Keywords

Petri nets; formal verification; reachability analysis; real-time systems; specification languages; algorithmic aspects; formal models; hierarchical development; hierarchical verification; high-level timed Petri nets; highly expressive graphical specification languages; problem-oriented characteristics; real-time systems; structured analysis methods; system requirements; user-friendly characteristics; Analytical models; Joining processes; Petri nets; Power system modeling; Real time systems; Safety; Specification languages; System analysis and design;

fLanguage

English

Publisher

ieee

Conference_Titel

Systems, Man, and Cybernetics, 1997. Computational Cybernetics and Simulation., 1997 IEEE International Conference on

Conference_Location

Orlando, FL

ISSN

1062-922X

Print_ISBN

0-7803-4053-1

Type

conf

DOI

10.1109/ICSMC.1997.635201

Filename

635201