{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:38Z","timestamp":1740134558760,"version":"3.37.3"},"reference-count":17,"publisher":"Wiley","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/501100002338","name":"Ministry of Education of the People\u2019s Republic of China","doi-asserted-by":"publisher","award":["61171121"],"award-info":[{"award-number":["61171121"]}],"id":[{"id":"10.13039\/501100002338","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61171121"],"award-info":[{"award-number":["61171121"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2014]]},"abstract":"<jats:p>The efficiency of the compositional verification of invariants depends on the abstraction, which may lead to verification incompleteness. The invariant strengthening and state partitioning techniques are proposed in this paper. The former could refine the overapproximation by removing the unreachable states, and the latter is a variant of counterexample-guided abstraction refinement. Integrated with these two refinement techniques, a unified compositional verification framework is presented to strengthen the abstraction and find counterexamples. Some examples are included to show that the verification of the safety properties in component-based systems has been achieved by our framework.<\/jats:p>","DOI":"10.1155\/2014\/703098","type":"journal-article","created":{"date-parts":[[2014,6,11]],"date-time":"2014-06-11T17:26:46Z","timestamp":1402507606000},"page":"1-12","source":"Crossref","is-referenced-by-count":1,"title":["Compositional Abstraction Refinement for Component-Based Systems"],"prefix":"10.1155","volume":"2014","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7649-3110","authenticated-orcid":true,"given":"Lianyi","family":"Zhang","sequence":"first","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0067-0341","authenticated-orcid":true,"given":"Qingdi","family":"Meng","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]},{"given":"Kueiming","family":"Lo","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]}],"member":"311","reference":[{"year":"1989","key":"1"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028755"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80004-0"},{"first-page":"213","volume-title":"Thread-modular model checking","year":"2003","key":"4"},{"first-page":"356","volume-title":"Thread-modular counterexample-guided abstraction refinement","year":"2011","key":"5"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_27"},{"issue":"6","key":"7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/996893.996844","volume":"39","year":"2004","journal-title":"ACM SIGPLAN Notices"},{"first-page":"505","volume-title":"Invest: a tool for the verification of invariants","year":"1998","key":"8"},{"first-page":"82","volume-title":"Automatic deductive verification with invisible invariants","year":"2001","key":"9"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_19"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen.2009.0011"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2010.2069102"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008744030390"},{"year":"1981","key":"15","first-page":"x+290"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55676-1_4"},{"first-page":"113","volume-title":"A technique for invariant generation","year":"2001","key":"17"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/703098.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/703098.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/703098.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T10:43:45Z","timestamp":1498128225000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2014\/703098\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":17,"alternative-id":["703098","703098"],"URL":"https:\/\/doi.org\/10.1155\/2014\/703098","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2014]]}}}