{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T00:58:32Z","timestamp":1768525112969,"version":"3.49.0"},"reference-count":60,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"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":["Journal of Systems and Software"],"published-print":{"date-parts":[[1995,1]]},"DOI":"10.1016\/0164-1212(94)00082-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T12:47:59Z","timestamp":1027601279000},"page":"77-87","source":"Crossref","is-referenced-by-count":19,"title":["The practice of formal methods in safety-critical systems"],"prefix":"10.1016","volume":"28","author":[{"given":"Shaoying","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victoria","family":"Stavridou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Dutertre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0164-1212(94)00082-X_BIB1","series-title":"VDM'91 Formal Software Development Methods","first-page":"398","article-title":"The B Method","author":"Abrial","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB2","series-title":"APR 926, Design Analysis Procedure for Failure Modes, Effects and Criticality Analysis (FMECA)","year":"1967"},{"key":"10.1016\/0164-1212(94)00082-X_BIB3","author":"Austin","year":"1993"},{"key":"10.1016\/0164-1212(94)00082-X_BIB4","first-page":"2","article-title":"Structuring for the VDM Specification Language","author":"Bear","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB5","author":"Bj\u00f8rner","year":"1982"},{"key":"10.1016\/0164-1212(94)00082-X_BIB6","article-title":"The RAISE Project-Fundamental Issues and Requirements","author":"Bj\u00f8rner","year":"1985"},{"key":"10.1016\/0164-1212(94)00082-X_BIB7","article-title":"Formal Methods: Epideictic or Apodeictic?","author":"Bowen","year":"1993","journal-title":"Software Eng. J."},{"key":"10.1016\/0164-1212(94)00082-X_BIB8","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1049\/sej.1993.0025","article-title":"Safety-Critical Systems, Formal Methods and Standards","volume":"8","author":"Bowen","year":"1993","journal-title":"Software Eng. J."},{"key":"10.1016\/0164-1212(94)00082-X_BIB9","series-title":"Proceedings of the Conference on Probabilistic Safety, Assessment and Management","article-title":"An application of fault tree analysis to safety-critical software at Ontario Hydro","author":"Bowman","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB10","article-title":"Report on the Formal Specification and Partial Verification of the VIPER Microprocessor","author":"Brock","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB11","series-title":"Proceedings of the 1989 Z User Meeting","article-title":"Using Z to Develop a CASE Toolset","author":"Brownbridge","year":"1989"},{"key":"10.1016\/0164-1212(94)00082-X_BIB12","series-title":"Proceedings of the 12th International Conference on Computer Safety, Reliability and Security","article-title":"Validating safety models with fault trees","author":"Bruns","year":"1993"},{"key":"10.1016\/0164-1212(94)00082-X_BIB13","article-title":"Reliability Computation Using Fault Trees","author":"Chelson","year":"1971"},{"key":"10.1016\/0164-1212(94)00082-X_BIB14","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1049\/sej.1993.0028","article-title":"Software Fault Trees and Weakest Preconditions: A Comparison and Analysis","author":"Clarke","year":"1993","journal-title":"Software Eng. J."},{"key":"10.1016\/0164-1212(94)00082-X_BIB15","series-title":"VLSI Specification, Verification and Synthesis","article-title":"A proof of correctness of the Viper microprocessor: The first level","author":"Cohn","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB16","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF00243000","article-title":"The Notion of Proof in Hardware Verification","volume":"5","author":"Cohn","year":"1989","journal-title":"J. Automat. Reason."},{"key":"10.1016\/0164-1212(94)00082-X_BIB17","article-title":"Introducing Formal Methods: The CICS Experience with Z","author":"Collins","year":"1987","journal-title":"IBM Technical Report TR 12.260"},{"key":"10.1016\/0164-1212(94)00082-X_BIB18","article-title":"An International Survey of International Applications of Formal Methods","author":"Craigen","year":"1993","journal-title":"Volume 2: Case Studies, NIST-GER 93\/626"},{"key":"10.1016\/0164-1212(94)00082-X_BIB19","first-page":"133","article-title":"Application of Formal Methods to the VIPER Microprocessor","volume":"134","author":"Cullyer","year":"1987"},{"key":"10.1016\/0164-1212(94)00082-X_BIB20","article-title":"Formal Specification and Structured Design in Software Development","author":"Cyrus","year":"1991","journal-title":"Hewlett-Packard J."},{"key":"10.1016\/0164-1212(94)00082-X_BIB21","first-page":"29","article-title":"A Formal Specification of an Oscilloscope","author":"Delisle","year":"1990","journal-title":"IEEE Software"},{"key":"10.1016\/0164-1212(94)00082-X_BIB22","author":"Dyer","year":"1992"},{"key":"10.1016\/0164-1212(94)00082-X_BIB23","volume":"1","author":"Ehrig","year":"1985"},{"key":"10.1016\/0164-1212(94)00082-X_BIB24","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0164-1212(93)90029-W","article-title":"Safety Case: An Integrated Toolset For Software Safety Analysis","volume":"21","author":"Fenelon","year":"1993","journal-title":"J. Syst. Software"},{"key":"10.1016\/0164-1212(94)00082-X_BIB25","series-title":"Proceedings of Safety-Critical Systems Symposium 1993","article-title":"SAM\u2014A tool to support the construction, review and evolution of safety arguments","author":"Forder","year":"1993"},{"key":"10.1016\/0164-1212(94)00082-X_BIB26","series-title":"VDM 90: VDM and Z!","first-page":"150","article-title":"Formal specifications as reusable frameworks","author":"Garlan","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB27","series-title":"Proceedings of IEEE Conference on Specification for Reliable Software","first-page":"170","article-title":"An introduction to OBJ: A language for writing and testing formal algebraic program specifications","author":"Goguen","year":"1979"},{"key":"10.1016\/0164-1212(94)00082-X_BIB28","article-title":"Introducing OBJ3","author":"Goguen","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB29","series-title":"VLSI Specification, Verification and Synthesis","first-page":"73","article-title":"HOL: A proof generating system for high order logic","author":"Gordon","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB30","series-title":"International Conference on Software Engineering","article-title":"SACEM software validation","author":"Guiho","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB31","series-title":"Proceedings of Colloquium on Analysis of Requirements for Software Intensive Systems","article-title":"Linking fault trees to software specifications","author":"Hansen","year":"1993"},{"key":"10.1016\/0164-1212(94)00082-X_BIB32","first-page":"500","article-title":"SmartCard Technology: New Methods for Computer Access Control","author":"Haykin","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB33","first-page":"80","article-title":"PES\u2014Programmable electronic systems in safety related applications","author":"Health Safety Executive","year":"1987"},{"key":"10.1016\/0164-1212(94)00082-X_BIB34","series-title":"Second IEE\/BCS Conference, Software Engineering 88","first-page":"169","article-title":"The development of high reliability software-RR and A's experience for safety critical systems","author":"Hill","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB35","series-title":"Proceedings of the 6th Annual Conference on Computer Assurance (COMPASS)","article-title":"Software development methods in practice","author":"Hill","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB36","author":"Hoare","year":"1985"},{"key":"10.1016\/0164-1212(94)00082-X_BIB37","first-page":"588","article-title":"CICS project report: Experiences and results from the use of Z","volume":"vol. 551","author":"Houston","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB38","author":"Jones","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB39","author":"Jones","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB40","first-page":"164","article-title":"Z and the refinement calculus","author":"King","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB41","series-title":"6th Computer Security Applications Conference","article-title":"Formal specification and verification of control software for cryptographic equipment","author":"Kuhn","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB42","article-title":"Experiences from Applications of RAISE","author":"LACOS","year":"1992","journal-title":"LACOS Project Reports LA-COS\/CRI\/CONS\/13\/V1 and LACOS\/CRI\/CONS\/20\/V1, 1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB43","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1109\/TSE.1983.235116","article-title":"Analyzing Software Safety","volume":"SE-9","author":"Leveson","year":"1983","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0164-1212(94)00082-X_BIB44","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0164-1212(83)90030-4","article-title":"Software Fault Tree Analysis","volume":"1983","author":"Leveson","year":"1983","journal-title":"J. Syst. Software"},{"key":"10.1016\/0164-1212(94)00082-X_BIB45","series-title":"CompSac","article-title":"A case study in cleanroom software engineering: The IBM COBOL structuring facility","author":"Linger","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB46","article-title":"Software Engineering Laboratory (SEL): Cleanroom Process Model","author":"Linger","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB47","series-title":"Proceedings of the Safety-Critical Systems Symposium","first-page":"217","article-title":"The need for evidence from disparate sources to evaluate software safety","author":"Littlewood","year":"1993"},{"key":"10.1016\/0164-1212(94)00082-X_BIB48","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0164-1212(93)90037-X","article-title":"A Formal Requirements Specification Method Based on Data Flow Analysis","author":"Liu","year":"1993","journal-title":"J. Syst. Software"},{"key":"10.1016\/0164-1212(94)00082-X_BIB49","unstructured":"Liu, S., Internal Consistency of FRSM, J. Syst. Software (in press)."},{"key":"10.1016\/0164-1212(94)00082-X_BIB50","article-title":"The Procurement of Safety Critical Software In Defence Equipment","author":"Ministry of Defence","year":"1991"},{"key":"10.1016\/0164-1212(94)00082-X_BIB51","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/BF01212405","article-title":"The Formal Specification of Safety Requirements for Storing Explosives","volume":"5","author":"Mukherjee","year":"1993","journal-title":"Formal Aspects Comp."},{"key":"10.1016\/0164-1212(94)00082-X_BIB52","first-page":"103","article-title":"The Use of Software Engineering, Including the Z Notation, in the Development of CICS","volume":"14","author":"Nix","year":"1988","journal-title":"Quality Assur."},{"key":"10.1016\/0164-1212(94)00082-X_BIB53","year":"1993","journal-title":"A Technical Overview of CDIS, PRAXIS CDIS Technical Overview"},{"key":"10.1016\/0164-1212(94)00082-X_BIB54","series-title":"VDM\u2014A Formal Method at Work","first-page":"141","article-title":"From VDM to RAISE","author":"Prehn","year":"1987"},{"key":"10.1016\/0164-1212(94)00082-X_BIB55","series-title":"IRSM'90","first-page":"1","article-title":"Software system failure mode and effects analysis (SSFMEA)\u2014A tool for reliability growth","author":"Raheja","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB56","article-title":"Case Studies in HP-SL","author":"Rush","year":"1990"},{"key":"10.1016\/0164-1212(94)00082-X_BIB57","series-title":"Understanding Z: A Specification Language and its Formal Semantics","author":"Spivey","year":"1988"},{"key":"10.1016\/0164-1212(94)00082-X_BIB58","author":"Spivey","year":"1989"},{"key":"10.1016\/0164-1212(94)00082-X_BIB59","author":"Toulmin","year":"1958"},{"key":"10.1016\/0164-1212(94)00082-X_BIB60","author":"Veseley","year":"1981"}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016412129400082X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016412129400082X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T06:26:00Z","timestamp":1556605560000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/016412129400082X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["016412129400082X"],"URL":"https:\/\/doi.org\/10.1016\/0164-1212(94)00082-x","relation":{},"ISSN":["0164-1212"],"issn-type":[{"value":"0164-1212","type":"print"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}