Title :
Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
Author :
Yang, Stephen J H ; Chu, William ; Lin, Sam ; Lee, Jonathan
Author_Institution :
Dept. of Comput. Sci. & Inf. Eng., Nat. Central Univ., Chung-Li, Taiwan
Abstract :
The paper presents our reachability tree logic (RTL) and its integration with temporal Petri nets to specify and verify the temporal behavior of high assurance systems. In addition, we demonstrate how to reduce the complexity of a model checking algorithm by using the reachability tree. We have implemented a specification and verification toolkit called NCUPN (National Central University Petri Nets toolkit) using Java. NCUPN is now available on the Internet via http://140.115.50.137
Keywords :
Java; Petri nets; formal specification; program verification; reachability analysis; software reliability; temporal logic; trees (mathematics); Java; NCUPN; National Central University Petri Nets toolkit; high assurance systems; model checking algorithm; reachability tree logic; temporal Petri nets; temporal behavior specification; temporal behavior verification; verification toolkit; Logic;
Conference_Titel :
High-Assurance Systems Engineering Symposium, 1998. Proceedings. Third IEEE International
Conference_Location :
Washington, DC
Print_ISBN :
0-8186-9221-9
DOI :
10.1109/HASE.1998.731607
