{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:50:43Z","timestamp":1758981043232},"reference-count":27,"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":[[2011,3]]},"abstract":"<jats:p> Software risk comes mainly from its poor reliability, but how to effectively achieve high reliability still remains a challenge. This paper puts forward a framework for systematically integrating formal specification, review, and testing, and shows how it can be applied to effectively eliminate errors in the major phases of software development process to enhance software reliability. In this framework, requirements errors can be removed and missing requirements can be identified by formalizing requirements into formal specifications whose validity can be ensured by rigorous review. The valid specification can then be used as a firm foundation for implementation and for rigorous inspection, testing, and walkthrough of the implemented program. We discuss how formalization, review, and testing work together at different levels of software development to improve software reliability through detecting and removing errors in documentation. <\/jats:p>","DOI":"10.1142\/s0218194011005268","type":"journal-article","created":{"date-parts":[[2011,6,7]],"date-time":"2011-06-07T11:28:30Z","timestamp":1307446110000},"page":"259-288","source":"Crossref","is-referenced-by-count":10,"title":["A FRAMEWORK FOR INTEGRATING FORMAL SPECIFICATION, REVIEW, AND TESTING TO ENHANCE SOFTWARE RELIABILITY"],"prefix":"10.1142","volume":"21","author":[{"given":"SHAOYING","family":"LIU","sequence":"first","affiliation":[{"name":"Department of Computer Science, Hosei University, Tokyo 184-8584, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"TETSUO","family":"TAMAI","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SHIN","family":"NAKAJIMA","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","volume-title":"Industrial Applications of Formal Methods to Model, Design and Analyze Computer Systems: An International Survey","author":"Craigen D.","year":"1995"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1109\/52.506463"},{"key":"rf3","volume-title":"Object-Oriented Analysis and Design with Applications","author":"Booch G.","year":"1994"},{"key":"rf4","volume-title":"Programming from Specifications","author":"Morgan C.","year":"1994"},{"key":"rf5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"rf6","volume-title":"Systematic Software Development Using VDM","author":"Jones C. B.","year":"1990"},{"key":"rf7","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock J.","year":"1996"},{"key":"rf8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"rf11","volume-title":"Software Inspection: An Industry Best Practice","author":"Wheeler D. A.","year":"1996"},{"key":"rf12","volume-title":"Software Quality: Producing Practical, Consistent Software","author":"Menachem M. B.","year":"1997"},{"key":"rf13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07287-5"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"rf15","volume-title":"VDMTOOLS for Quality Software on Schedule \u2014 VDM-SL Toolbox User Manual, The IFAD VDM-SL Language","author":"IFAD","year":"1999"},{"key":"rf16","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00166-X"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"rf20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018913028597"},{"key":"rf21","volume-title":"Model Checking","author":"Clarke E. M.","year":"2000"},{"key":"rf22","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"key":"rf24","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"key":"rf27","series-title":"Advances in Computers","volume-title":"Software Process","volume":"42","author":"Porter A.","year":"1995"},{"key":"rf28","doi-asserted-by":"publisher","DOI":"10.1007\/11498490_15"},{"key":"rf31","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.264"},{"key":"rf35","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2006.12.540"},{"key":"rf38","first-page":"387","author":"Bernot G.","journal-title":"Software Engineering Journal"},{"key":"rf39","doi-asserted-by":"publisher","DOI":"10.1109\/32.553698"},{"key":"rf40","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(99)00066-7"},{"key":"rf41","doi-asserted-by":"publisher","DOI":"10.1109\/32.368133"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194011005268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T16:12:16Z","timestamp":1565194336000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194011005268"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":27,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2011,3]]}},"alternative-id":["10.1142\/S0218194011005268"],"URL":"https:\/\/doi.org\/10.1142\/s0218194011005268","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3]]}}}