{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T04:57:42Z","timestamp":1648616262972},"reference-count":0,"publisher":"World Scientific Pub Co Pte Lt","issue":"02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[1999,4]]},"abstract":"<jats:p> 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\u2032 and obtain a RT\u2032 of the modified N\u2032. The modification (refinement) continues until the modified RT\u2032 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 <\/jats:p>","DOI":"10.1142\/s0218194099000152","type":"journal-article","created":{"date-parts":[[2003,2,24]],"date-time":"2003-02-24T10:42:33Z","timestamp":1046083353000},"page":"233-249","source":"Crossref","is-referenced-by-count":0,"title":["SPECIFYING AND VERIFYING TEMPORAL BEHAVIOR OF HIGH ASSURANCE SYSTEMS USING REACHABILITY TREE LOGIC"],"prefix":"10.1142","volume":"09","author":[{"given":"STEPHEN J. H.","family":"YANG","sequence":"first","affiliation":[{"name":"Department of Computer Science and Information Engineering, National Central University, Taiwan, ROC"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"WILLIAM","family":"CHU","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Information Engineering, National Central University, Taiwan, ROC"},{"name":"Department of Computer and Information Science, TungHai University, Taiwan, ROC"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JONATHAN","family":"LEE","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Information Engineering, National Central University, Taiwan, ROC"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194099000152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T16:12:08Z","timestamp":1565194328000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194099000152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,4]]},"references-count":0,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[1999,4]]}},"alternative-id":["10.1142\/S0218194099000152"],"URL":"https:\/\/doi.org\/10.1142\/s0218194099000152","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,4]]}}}