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

S. J.H. Yang, W. Chu, S. Lin, J. Lee

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationProceedings - 3rd IEEE International High-Assurance Systems Engineering Symposium, HASE 1998
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages150-156
Number of pages7
ISBN (Electronic)0818692219, 9780818692215
DOIs
StatePublished - 1998
Event3rd IEEE International High-Assurance Systems Engineering Symposium, HASE 1998 - Washington, United States
Duration: 13 Nov 199814 Nov 1998

Publication series

NameProceedings - 3rd IEEE International High-Assurance Systems Engineering Symposium, HASE 1998
Volume1998-November

Conference

Conference3rd IEEE International High-Assurance Systems Engineering Symposium, HASE 1998
Country/TerritoryUnited States
CityWashington
Period13/11/9814/11/98

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