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

Stephen J.H. Yang, William Chu, Jonathan Lee

研究成果: 雜誌貢獻期刊論文同行評審

摘要

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://140.115.155.46.

原文???core.languages.en_GB???
頁(從 - 到)233-249
頁數17
期刊International Journal of Software Engineering and Knowledge Engineering
9
發行號2
DOIs
出版狀態已出版 - 4月 1999

指紋

深入研究「Specifying and verifying temporal behavior of high assurance systems using reachability tree logic」主題。共同形成了獨特的指紋。

引用此