Specifying and Verifying Temporal Behavior of High Assurance Systems Using Reachability Tree Logic.
Journal
3rd IEEE International Symposium on High-Assurance Systems Engineering (HASE '98), 13-14 November 1998, Washington, D.C, USA, Proceedings
Pages
150-157
Date Issued
1998
Author(s)
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.
SDGs
Type
conference paper