{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:27:51Z","timestamp":1767983271272,"version":"3.49.0"},"reference-count":16,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Reliability Engineering & System Safety"],"published-print":{"date-parts":[[2003,10]]},"DOI":"10.1016\/s0951-8320(03)00059-0","type":"journal-article","created":{"date-parts":[[2003,8,8]],"date-time":"2003-08-08T06:13:54Z","timestamp":1060323234000},"page":"11-20","source":"Crossref","is-referenced-by-count":12,"title":["Systematic evaluation of fault trees using real-time model checker UPPAAL"],"prefix":"10.1016","volume":"82","author":[{"given":"Sungdeok","family":"Cha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanseong","family":"Son","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junbeom","family":"Yoo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eunkyung","family":"Jee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Poong Hyun","family":"Seong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0951-8320(03)00059-0_BIB1","series-title":"Technical report NUREG-0492","author":"Vesely","year":"1981"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB2","series-title":"Safeware: system safety and computers","author":"Leveson","year":"1995"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB3","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/RAMS.1997.571667","article-title":"Automatic fault-tree synthesis and real-time trimming, based on computer models","author":"Kocza","year":"1997","journal-title":"Proc Ann Reliab Maintainability Symp"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB4","unstructured":"WWW formal technical review (FTR) Archive, http:\/\/www.ics.hawaii.edu\/~johnson\/FTR\/."},{"key":"10.1016\/S0951-8320(03)00059-0_BIB5","series-title":"Model checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB6","series-title":"Symbolic model checking: an approach to the state explosion problem","author":"McMillan","year":"1993"},{"issue":"5","key":"10.1016\/S0951-8320(03)00059-0_BIB7","doi-asserted-by":"crossref","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzman","year":"1997","journal-title":"IEEE Trans Software Engng"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB8","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Larsen KG, Larsson F, Pettersson P, Yi W. UPPAAL: a tool suite for automatic verification of real-time systems. Proceedings of the Fourth DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, NJ; October 1995.","DOI":"10.1007\/BFb0020949"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB9","doi-asserted-by":"crossref","unstructured":"Pnueli A. The temporal logic of programs. Proceedings of the 18th IEEE Symposium on Foundations of Computer Science; 1977. p. 46\u201377.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB10","unstructured":"Program functional specification, SDS2 programmable digital comparators, Wolsong NPP 2,3,4. Technical Report 86-68300-PFS-000 Rev. 2, AECL CANDU; May 1993."},{"key":"10.1016\/S0951-8320(03)00059-0_BIB11","unstructured":"Software requirement specification, SDS2 programmable digital comparators, Wolsong NPP 2,3,4. Technical report 86-68350-SRS-001 Rev. 0, AECL CANDU; June 1993."},{"key":"10.1016\/S0951-8320(03)00059-0_BIB12","unstructured":"Software design description, SDS2 programmable digital comparators, Wolsong NPP 2,3,4. Technical report 86-68350-SDD-001 Rev. 0, AECL CANDU; December 1993."},{"key":"10.1016\/S0951-8320(03)00059-0_BIB13","unstructured":"Moss TJ. Quantitative techniques for nuclear plant safety assessment and design. Meeting on Nuclear Power Reactor Safety, Brussels, Belgium; 16 Oct 1978.s."},{"issue":"3","key":"10.1016\/S0951-8320(03)00059-0_BIB14","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1002\/qre.405","article-title":"The use of not logic in fault tree analysis","volume":"17","author":"Andrews","year":"2001","journal-title":"Qty Reliab Engng Int"},{"issue":"2","key":"10.1016\/S0951-8320(03)00059-0_BIB15","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"Automata for modeling real-time systems","volume":"126","author":"Alur","year":"1994","journal-title":"Theor Comput Sci"},{"key":"10.1016\/S0951-8320(03)00059-0_BIB16","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","article-title":"The temporal logic of branching time","volume":"20","author":"Ben-Ari","year":"1983","journal-title":"Acta Inform"}],"container-title":["Reliability Engineering & System Safety"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0951832003000590?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0951832003000590?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,25]],"date-time":"2020-03-25T05:47:05Z","timestamp":1585115225000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0951832003000590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,10]]}},"alternative-id":["S0951832003000590"],"URL":"https:\/\/doi.org\/10.1016\/s0951-8320(03)00059-0","relation":{},"ISSN":["0951-8320"],"issn-type":[{"value":"0951-8320","type":"print"}],"subject":[],"published":{"date-parts":[[2003,10]]}}}