{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T17:19:16Z","timestamp":1771003156141,"version":"3.50.1"},"reference-count":11,"publisher":"SAGE Publications","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCM"],"published-print":{"date-parts":[[2020,4,10]]},"DOI":"10.3233\/jcm-193773","type":"journal-article","created":{"date-parts":[[2019,8,16]],"date-time":"2019-08-16T11:36:12Z","timestamp":1565955372000},"page":"217-226","source":"Crossref","is-referenced-by-count":0,"title":["Checking the consistency of Object-Z formal specification based on theorem proof"],"prefix":"10.1177","volume":"20","author":[{"given":"Weiqing","family":"Wan","sequence":"first","affiliation":[]},{"given":"Yongqing","family":"Yu","sequence":"additional","affiliation":[]},{"given":"Qingyan","family":"Zeng","sequence":"additional","affiliation":[]},{"given":"Zhicheng","family":"Wen","sequence":"additional","affiliation":[]}],"member":"179","reference":[{"issue":"6","key":"10.3233\/JCM-193773_ref3","first-page":"1770","article-title":"Modeling and verification of services oriented cyber physical systems","volume":"34","author":"Liu","year":"2014","journal-title":"Journal of Computer Applications"},{"issue":"2","key":"10.3233\/JCM-193773_ref4","first-page":"223","article-title":"Software formal modeling and verification method based on time STM","volume":"26","author":"Hou","year":"2015","journal-title":"Journal of Software"},{"issue":"4","key":"10.3233\/JCM-193773_ref5","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1109\/TNSRE.2019.2893152","article-title":"Improving reliability of myocontrol using Formal Verification","volume":"27","author":"Guidotti","year":"2019","journal-title":"IEEE Transactions on Neural Systems and Rehabilitation Engineering"},{"issue":"1","key":"10.3233\/JCM-193773_ref6","first-page":"140","article-title":"Formal modeling and verification of resource-oriented internet of things systems","volume":"39","author":"Ma","year":"2018","journal-title":"Journal of Chinese Computer Systems"},{"issue":"4","key":"10.3233\/JCM-193773_ref8","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/j.scico.2008.09.012","article-title":"Checking the CICS file control API with Z\/EVES: an experiment in the verified software repository","volume":"74","author":"Freitas","year":"2009","journal-title":"Science of Computer Programming"},{"key":"10.3233\/JCM-193773_ref9","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-642-16901-4_5","article-title":"Theorem proof generation and discharging for recursive definitions in VDM","author":"Ribeiro","year":"2010","journal-title":"Formal Methods and Software Engineering"},{"key":"10.3233\/JCM-193773_ref10","unstructured":"S. Katz and A. Rashid, From aspectual requirements to theorem proofs for aspect-oriented systems, in: 12th IEEE International (RE\u201904), 2004, pp, 48\u201357."},{"key":"10.3233\/JCM-193773_ref11","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-540-87603-8_11","article-title":"On the purpose of Event-B theorem proofs","author":"Hallerstede","year":"2008","journal-title":"Abstract State Machines, B and Z"},{"issue":"6","key":"10.3233\/JCM-193773_ref12","first-page":"2031","article-title":"Formal transformation and verification of UML model based on specification Z","volume":"34","author":"Zhang","year":"2013","journal-title":"Computer Engineering and Design"},{"issue":"6","key":"10.3233\/JCM-193773_ref13","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.3724\/SP.J.1001.2011.04021","article-title":"Automatic test case generator for Object-Z specification","volume":"22","author":"Xu","year":"2011","journal-title":"Journal of Software"},{"issue":"1","key":"10.3233\/JCM-193773_ref14","first-page":"193","article-title":"Method for generating formal interlocking software model based on scenario","volume":"42","author":"Dong","year":"2015","journal-title":"Computer Science"}],"container-title":["Journal of Computational Methods in Sciences and Engineering"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCM-193773","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T16:31:34Z","timestamp":1771000294000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/JCM-193773"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,10]]},"references-count":11,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.3233\/jcm-193773","relation":{},"ISSN":["1472-7978","1875-8983"],"issn-type":[{"value":"1472-7978","type":"print"},{"value":"1875-8983","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,10]]}}}