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 http://18.104.22.168.
|頁（從 - 到）||233-249|
|期刊||International Journal of Software Engineering and Knowledge Engineering|
|出版狀態||已出版 - 4月 1999|