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://188.8.131.52
Keywords: NCUPT toolkit, Petri nets, RTL, formal methods, high-assurance systems, temporal logic.
Back to the Petri Nets Bibliography