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

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

Research output: Contribution to journalArticlepeer-review

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

Original languageEnglish
Pages (from-to)233-249
Number of pages17
JournalInternational Journal of Software Engineering and Knowledge Engineering
Volume9
Issue number2
DOIs
StatePublished - Apr 1999

Keywords

  • Formal methods
  • High assurance systems
  • Petri nets
  • Specification
  • Temporal logic
  • Verification

Fingerprint

Dive into the research topics of 'Specifying and verifying temporal behavior of high assurance systems using reachability tree logic'. Together they form a unique fingerprint.

Cite this