Specifying and Verifying Temporal Behavior of High Assurance Systems Using Reachability Tree Logic.
Journal
International Journal of Software Engineering and Knowledge Engineering
Journal Volume
9
Journal Issue
2
Pages
233-249
Date Issued
1999
Author(s)
Abstract
This paper presents our reachability tree logic (RTL) and its integration with time Petri nets to specify and verify the temporal behavior of high assurance systems. The specification phase begins with a system modeling to model system requirements into a time Petri net N and construct a reachability tree RT of N. We then use RTL to specify the desired temporal behavior as formula F. The verification phase uses a model-checking algorithm to check whether RT can satisfy F, that is to find firing sequences to satisfy F. If F is not satisfied, we then modify N into N′ and obtain a RT′ of the modified N′. The modification (refinement) continues until the modified RT′ can satisfy F. In addition, we will demonstrate how to reduce the complexity of model-checking by using our RTL-based algorithm. 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
Type
journal article