{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:42:17Z","timestamp":1740181337199,"version":"3.37.3"},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T00:00:00Z","timestamp":1637712000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T00:00:00Z","timestamp":1637712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100012403","name":"Central University Basic Scientific Research Business Expenses Special Funds","doi-asserted-by":"publisher","award":["DUT2019ZD104"],"award-info":[{"award-number":["DUT2019ZD104"]}],"id":[{"id":"10.13039\/501100012403","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["CCF Trans. HPC"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s42514-021-00082-9","type":"journal-article","created":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T15:02:51Z","timestamp":1637766171000},"page":"365-382","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["EHSTM: a formal model of embedded software and research on several key issues"],"prefix":"10.1007","volume":"3","author":[{"given":"Watanabe","family":"Masahiko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9437-9434","authenticated-orcid":false,"given":"Kuanjiu","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yicong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zizhong","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junyu","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,24]]},"reference":[{"key":"82_CR1","unstructured":"About the Unified Modeling Language specification Ver. 2.5. (2013) https:\/\/www.omg.org\/spec\/UML\/2.5\/About-UML\/"},{"issue":"1","key":"82_CR2","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1002\/cpe.3659","volume":"28","author":"PA Buhr","year":"2016","unstructured":"Buhr, P.A., Dice, D., Hesselink, W.H.: Dekker\u2019s mutual exclusion algorithm made RW-safe. Concurr. Comput. Pract. Exp. 28(1), 144\u2013165 (2016)","journal-title":"Concurr. Comput. Pract. Exp."},{"key":"82_CR3","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"82_CR4","unstructured":"Embedded System development Process Reference guide Ver.2.0 (2012) [2020] Written and edited by Software Engineering Center, Technology Headquarters, Information-technology Promotion Agency, Japan. https:\/\/www.ipa.go.jp\/files\/000028853.pdf. Accessed Jan 2012"},{"key":"82_CR5","unstructured":"ISO\/IEC11411 (1995) Information technology\u2014Representation for human communication of state transition of software"},{"key":"82_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01566-4","volume-title":"Ubiquitous Computing and Computing Security of IoT","author":"N Jeyanthi","year":"2019","unstructured":"Jeyanthi, N., Abraham, A., Mcheick, H.: Ubiquitous Computing and Computing Security of IoT. Springer, New York (2019)"},{"key":"82_CR7","doi-asserted-by":"crossref","unstructured":"Kamel, M., Karray, F., Gueaieb, W., Khamis, A.: Autonomous and intelligent systems. In: Second International Conference, AIS 2011, Burnaby, BC, Canada, June 22\u201324 (2011)","DOI":"10.1007\/978-3-642-21538-4"},{"key":"82_CR10","unstructured":"Masahiko, W.: Embedded software development environments. IPSJ Mag. 45(1), 10\u201315 (2004)"},{"key":"82_CR11","doi-asserted-by":"crossref","unstructured":"Sangiovanni-Vincentelli, A., Sifakis, J.: Embedded software. In: Second international conference, EMSOFT 2002 Grenoble, France, October 7\u20139 (2002)","DOI":"10.1007\/3-540-45828-X"},{"issue":"5","key":"82_CR12","doi-asserted-by":"publisher","first-page":"943","DOI":"10.1007\/s00165-013-0282-7","volume":"26","author":"Y Yamagata","year":"2014","unstructured":"Yamagata, Y., Kong, W., Fukuda, A., Van Tang, N., Ohsaki, H., Taguchi, K.: A formal semantics of extended hierarchical state transition matrices using CSP. Form. Aspects Comput. 26(5), 943\u2013962 (2014)","journal-title":"Form. Aspects Comput."}],"container-title":["CCF Transactions on High Performance Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42514-021-00082-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42514-021-00082-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42514-021-00082-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T08:29:31Z","timestamp":1638433771000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42514-021-00082-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,24]]},"references-count":10,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["82"],"URL":"https:\/\/doi.org\/10.1007\/s42514-021-00082-9","relation":{},"ISSN":["2524-4922","2524-4930"],"issn-type":[{"type":"print","value":"2524-4922"},{"type":"electronic","value":"2524-4930"}],"subject":[],"published":{"date-parts":[[2021,11,24]]},"assertion":[{"value":"23 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 September 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}