{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T05:00:14Z","timestamp":1698037214369},"reference-count":16,"publisher":"Wiley","issue":"8","license":[{"start":{"date-parts":[[2006,10,30]],"date-time":"2006-10-30T00:00:00Z","timestamp":1162166400000},"content-version":"vor","delay-in-days":5934,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Pract Exp"],"published-print":{"date-parts":[[1990,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe our practical experience in the use of formal verification to obtain increased confidence in the design of safety\u2010critical systems. The experiment involved demonstrating the consistency of the design specifications of SIFT, a software\u2010implemented fault\u2010tolerant operating system for aircraft flight control. Specifications were written at successive levels of abstraction from the most abstract requirements definition down to the detailed level of program code. Consistency of the successive levels of specification was demonstrated using the enhanced HDM verification system. Formal verification is currently feasible only for carefully simplified systems, but there appears to be no alternative method that can meet the extreme safety requirements for safety\u2010critical systems.<\/jats:p>","DOI":"10.1002\/spe.4380200804","type":"journal-article","created":{"date-parts":[[2006,11,18]],"date-time":"2006-11-18T00:46:16Z","timestamp":1163810776000},"page":"799-821","source":"Crossref","is-referenced-by-count":21,"title":["Formal verification of safety\u2010critical systems"],"prefix":"10.1002","volume":"20","author":[{"given":"Louise E.","family":"Moser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. M.","family":"Melliar\u2010Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2006,10,30]]},"reference":[{"key":"e_1_2_1_2_2","unstructured":"Advisory Circular 25.1309\u20131 \u2018System design analysis\u2019 U.S. Dept. of Transportation Federal Aviation Administration Washington D.C. September1982."},{"key":"e_1_2_1_3_2","unstructured":"J. R.Dunham \u2018Software errors in experimental systems having ultra\u2010reliability requirements\u2019 Proc. IEEE Symposium on Fault Tolerant Computing 1986 pp.158\u2013164."},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/7474.7528"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231893"},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312842"},{"key":"e_1_2_1_7_2","unstructured":"J. C.KnightandN. G.Leveson \u2018An empirical study of failure probabilities in multi\u2010version software\u2019 Proc. IEEE Symposium on Fault Tolerant Computing 1986 pp.165\u2013170."},{"key":"e_1_2_1_8_2","unstructured":"W. E.Vesely F. F.Goldberg N. H.RobertsandD. F.Haasl Fault Tree Handbook NUREG\u20100492 U.S. Nuclear Regulatory Commisssion January1981."},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1983.235116"},{"key":"e_1_2_1_10_2","doi-asserted-by":"crossref","unstructured":"J. B.GoodenoughandS. L.Gerhart \u2018Towards a theory of test data selection\u2019 Proc. SIGPLAN International Conf. on Reliable Software 1975 pp.493\u2013510.","DOI":"10.1145\/390016.808473"},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/356674.356677"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1978.11114"},{"key":"e_1_2_1_13_2","unstructured":"L. E.Moser P. M.Melliar\u2010SmithandR. L.Schwartz \u2018Design verification of SIFT\u2019 NASA Contractor Report Number 4079 September1987."},{"key":"e_1_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676059"},{"key":"e_1_2_1_15_2","unstructured":"J.Goldberg M. W.Green W. H.Kautz L. B.Lamport K. N.Levitt P. M.Melliar\u2010Smith R. L.SchwartzandC. B.Weinstock \u2018Development and analysis of the software implemented fault\u2010tolerance (SIFT) computer\u2019 NASA Contractor Report Number 172146 February1984."},{"key":"e_1_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0000050"},{"key":"e_1_2_1_17_2","volume-title":"Technical Report","author":"Crow J.","year":"1986"}],"container-title":["Software: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fspe.4380200804","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.4380200804","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T14:26:30Z","timestamp":1697984790000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/spe.4380200804"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,8]]},"references-count":16,"journal-issue":{"issue":"8","published-print":{"date-parts":[[1990,8]]}},"alternative-id":["10.1002\/spe.4380200804"],"URL":"https:\/\/doi.org\/10.1002\/spe.4380200804","archive":["Portico"],"relation":{},"ISSN":["0038-0644","1097-024X"],"issn-type":[{"value":"0038-0644","type":"print"},{"value":"1097-024X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,8]]}}}