{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,26]],"date-time":"2025-01-26T05:47:31Z","timestamp":1737870451795,"version":"3.33.0"},"edition-number":"1","reference-count":34,"publisher":"Wiley","isbn-type":[{"type":"print","value":"9780471383932"},{"type":"electronic","value":"9780470050118"}],"license":[{"start":{"date-parts":[[2009,3,16]],"date-time":"2009-03-16T00:00:00Z","timestamp":1237161600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/doi.wiley.com\/10.1002\/tdm_license_1.1"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Formal specifications of software components describe the behavior of components precisely using mathematically rigorous notations. They are necessary to avoid miscommunication between component developers and users, and avoid costly integration errors resulting from such miscommunication. They are also essential to facilitate formal verfication of correctness.<\/jats:p>","DOI":"10.1002\/9780470050118.ecse161","type":"other","created":{"date-parts":[[2008,1,15]],"date-time":"2008-01-15T14:46:25Z","timestamp":1200408385000},"page":"1307-1316","source":"Crossref","is-referenced-by-count":1,"title":["Formal Specification"],"prefix":"10.1002","author":[{"given":"Gregory","family":"Kulczycki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kimberly","family":"Roche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nighat","family":"Yasmin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2009,3,16]]},"reference":[{"key":"e_1_2_7_2_1","first-page":"21","volume-title":"Special Feature: Component\u2010Based Software Using RESOLVE, ACM SIGSOFT Software Engineering Notes 19, No. 4","author":"Sitaraman M.","year":"1994"},{"key":"e_1_2_7_3_1","doi-asserted-by":"crossref","unstructured":"M.Sitaraman S.Atkinson G.Kulczyski B. W.Weide T. J.Long P.Bucci W.Heym S.Pike J.Hollingsworth Reasoning about software\u2010component behavior Proceedings of the Sixth International Conference on Software Reuse Springer Verlag Vienna Austria 2000 pp.266\u2013283.","DOI":"10.1007\/978-3-540-44995-9_16"},{"key":"e_1_2_7_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"},{"volume-title":"Systematic Software Development using VDM","year":"1990","author":"Jones C. B.","key":"e_1_2_7_5_1"},{"volume-title":"The Z Notation: A Reference Manual","year":"1992","author":"Spivey J. M.","key":"e_1_2_7_6_1"},{"key":"e_1_2_7_6_2","unstructured":"Available at:http:\/\/spivey.oriel.ox.ac.uk\/mike\/zrm\/index.html."},{"key":"e_1_2_7_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"e_1_2_7_8_1","unstructured":"K. R. M.Leino G.Nelson J. B.Saxe ESC\/Java User's Manual.Technical Note 2000\u2013002 Compaq Systems Research Center 2000."},{"key":"e_1_2_7_9_1","first-page":"185","volume-title":"Science of Computer Programming","author":"Leavens G. T.","year":"2005"},{"key":"e_1_2_7_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"volume-title":"Reusable Software: The Base Object\u2010Oriented Component Libraries","year":"1994","author":"Meyer B.","key":"e_1_2_7_11_1"},{"key":"e_1_2_7_12_1","doi-asserted-by":"crossref","unstructured":"S.Owre N.Shankar J.Rushby PVS: A prototype verification system Proceedings CADE 11 Saratoga Springs NY 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_2_7_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_7_14_1","first-page":"1","volume-title":"Advances in Computers","author":"Weide B. W.","year":"1991"},{"key":"e_1_2_7_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.90445"},{"key":"e_1_2_7_16_1","doi-asserted-by":"crossref","unstructured":"A.Borgida J.Mylopoulos R.Reiter \u201c\u2026And nothing else changes\u201d: the frame problem in procedure specifications Proceedings of the 15th International Conference on Software Engineering Baltimore MD 1993 pp.303\u2013314.","DOI":"10.1109\/ICSE.1993.346034"},{"volume-title":"Proceedings SAVCBS 2006","year":"2006","author":"Krone J.","key":"e_1_2_7_17_1"},{"key":"e_1_2_7_18_1","doi-asserted-by":"crossref","unstructured":"M.Sitaraman T. J.Long T. J. B. W.Weide E. J.Harner L.Wang A formal approach to component\u2010based software engineering: education and evaluation Proceedings of the Twenty Third International Conference on Software Engineering IEEE 2001 601\u2013609.","DOI":"10.1109\/ICSE.2001.919134"},{"key":"e_1_2_7_19_1","unstructured":"B. W.Weide T. J.Long Software Component Engineering Course Sequence Home Page.Available:http:\/\/www.cse.ohio\u2010state.edu\/sce\/now\/."},{"key":"e_1_2_7_20_1","first-page":"11","volume-title":"Eighth International Symposium on the Foundations of Software Engineering","author":"Hollingsworth J.","year":"2000"},{"volume-title":"Formal Specification and Documentation Using Z: A Case Study Approach","year":"1996","author":"Bowen J.","key":"e_1_2_7_21_1"},{"key":"e_1_2_7_22_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1365-2966.2004.08451.x"},{"key":"e_1_2_7_23_1","unstructured":"VDM Specification Language 2007. Available:http:\/\/en.wikipedia.org\/wiki\/VDM_specification_language."},{"key":"e_1_2_7_24_1","doi-asserted-by":"crossref","unstructured":"M.Nielsen C.George The RAISE language method and tools Proceedings of the 2nd VDM\u2010Europe Symposium on VDM\u2014The Way Ahead Dublin Ireland 1988 pp.376\u2013405.","DOI":"10.1007\/3-540-50214-9_25"},{"key":"e_1_2_7_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/125083.123049"},{"key":"e_1_2_7_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/9758.10500"},{"key":"e_1_2_7_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_7_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"volume-title":"CASSIS 2004","year":"2004","author":"Barnett M.","key":"e_1_2_7_29_1"},{"key":"e_1_2_7_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/800127.804077"},{"key":"e_1_2_7_31_1","doi-asserted-by":"crossref","unstructured":"G. J.Popek J. J.Horning B. W.Lampson J. G.Mitchell R. L.London Notes on the design of Euclid Proceedings of an ACM Conference on Language Design for Reliable Software March 1977 pp.11\u201318.","DOI":"10.1145\/390019.808307"},{"key":"e_1_2_7_32_1","unstructured":"D. B.Wortman J. R.Cordy Early experiences with Euclid Proceedings ofICSE\u20105 IEEE Conference on Software Engineering San Diego CA 1981 pp.27\u201332."},{"key":"e_1_2_7_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9685-7"},{"key":"e_1_2_7_34_1","doi-asserted-by":"crossref","unstructured":"B.Carr? J.Garnsworthy SPARK\u2014an annotated Ada subset for safety\u2010critical programming Proceedings of the Conference on TRI\u2010ADA '90 TRI\u2010Ada '90 1990 pp.392\u2013402.","DOI":"10.1145\/255471.255563"}],"container-title":["Wiley Encyclopedia of Computer Science and Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/9780470050118.ecse161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T18:54:28Z","timestamp":1737831268000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/9780470050118.ecse161"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,16]]},"ISBN":["9780471383932","9780470050118"],"references-count":34,"alternative-id":["10.1002\/9780470050118.ecse161","10.1002\/9780470050118"],"URL":"https:\/\/doi.org\/10.1002\/9780470050118.ecse161","archive":["Portico"],"relation":{},"subject":[],"published":{"date-parts":[[2009,3,16]]}}}