{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T08:15:07Z","timestamp":1771661707907,"version":"3.50.1"},"reference-count":20,"publisher":"Zhejiang University Press","issue":"11","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61070226"],"award-info":[{"award-number":["61070226"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["springerlink.com","jzus.zju.edu.cn"],"crossmark-restriction":true},"short-container-title":["Frontiers Inf Technol Electronic Eng"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1631\/fitee.1601196","type":"journal-article","created":{"date-parts":[[2018,1,18]],"date-time":"2018-01-18T05:52:36Z","timestamp":1516254756000},"page":"1773-1783","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Mechanized semantics and refinement of UML-Statecharts"],"prefix":"10.1631","volume":"18","author":[{"given":"Feng","family":"Sheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3044-3841","authenticated-orcid":false,"given":"Liang","family":"Dou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zong-yuan","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"635","published-online":{"date-parts":[[2018,1,18]]},"reference":[{"key":"ref1","first-page":"335","article-title":"Using Coq to verify Java Card\u2122 applet isolation properties","volume-title":"Proc. Int. Conf. on Theorem Proving in Higher Order Logics","author":"Andronick"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44518-8_13"},{"key":"ref3","volume-title":"Towards a System Model for UML: the Structural Data Model","author":"Broy","year":"2007"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.2316\/p.2013.802-021"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24559-6_38"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"ref8","volume-title":"Secure Systems Development with UML","author":"Jurjens","year":"2005"},{"key":"ref9","first-page":"284","article-title":"Feature specification and refinement with state transition diagrams","volume-title":"Proc. 4th IEEE Workshop on Feature Interactions in Telecommunications Networks and Distributed Systems","author":"Klein"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.5220\/0001683700420049"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"issue":"5","key":"ref12","first-page":"563","article-title":"The CompCert C verified compiler: documentation and user\u2019s manual","volume":"16","author":"Leroy","year":"2015","journal-title":"Inria"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38613-8_23"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.04.006"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_37"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/s0167-6423(00)00026-5"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.14236\/ewic\/ROOM2000.8"},{"key":"ref18","first-page":"336","article-title":"UML-B and Event-B: an integration of languages and tools","volume-title":"Proc. IASTED Int. Conf. on Software Engineering","author":"Snook"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/sefm.2004.1347517"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0012-8"}],"container-title":["Frontiers of Information Technology & Electronic Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1631\/FITEE.1601196\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1631\/FITEE.1601196.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1631\/FITEE.1601196.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T07:31:09Z","timestamp":1771659069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1631\/FITEE.1601196"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":20,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["1177"],"URL":"https:\/\/doi.org\/10.1631\/fitee.1601196","relation":{},"ISSN":["2095-9184","2095-9230"],"issn-type":[{"value":"2095-9184","type":"print"},{"value":"2095-9230","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11]]},"assertion":[{"value":"http:\/\/orcid.org\/0000-0003-3044-3841","URL":"http","order":0,"name":"name","label":"Liang DOU","group":{"name":"orcid","label":"ORCID"}},{"value":"2016-04-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-06-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-11-29","order":2,"name":"crosschecked","label":"Crosschecked","group":{"name":"publication_history","label":"Publication History"}},{"value":"Article","order":0,"name":"content_type","group":{"name":"content_type","label":"Content Type"}},{"value":"\u00a9 Zhejiang University and Springer-Verlag GmbH Germany 2017","order":0,"name":"copyright","group":{"name":"copyright","label":"Copyright"}}]}}