For the most recent entries see the Petri Nets Newsletter.

Specifying and verifying temporal behavior of high assurance systems using reachability tree logic.

Yang, S.J.H.; Chu, W.; Lin, S.; Lee, J.

In: Proc. 3-rd Int. IEEE High-Assurance Systems Engineering Symposium, 13-14 November 1998, Washington, DC, pages 150-156. 1998.

Abstract: This paper presents reachability tree logic (RTL) and its integration with time Petri nets to specify and verify temporal behavior of high-assurance systems. In addition, the paper demonstrates how to reduce the complexity of model checking algorithm by using the reachability tree. A specification and verification toolkit, called NCUPN (National Central University Petri Net toolkit), has been implemented using Java. NCUPN is available on the Internet at http://140.115.50.137

Keywords: NCUPT toolkit, Petri nets, RTL, formal methods, high-assurance systems, temporal logic.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography