{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T05:29:17Z","timestamp":1732685357656,"version":"3.28.2"},"reference-count":13,"publisher":"SAGE Publications","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IFS"],"published-print":{"date-parts":[[2020,2,6]]},"DOI":"10.3233\/jifs-179502","type":"journal-article","created":{"date-parts":[[2019,11,8]],"date-time":"2019-11-08T18:28:17Z","timestamp":1573237697000},"page":"1391-1399","source":"Crossref","is-referenced-by-count":1,"title":["Formal verification of a task scheduler for embedded operating systems"],"prefix":"10.1177","volume":"38","author":[{"given":"Haiyong","family":"Sun","sequence":"first","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}]},{"given":"Hang","family":"Lei","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}]}],"member":"179","reference":[{"issue":"4","key":"10.3233\/JIFS-179502_ref1","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/s11390-010-1064-9","article-title":"Certification of thread context switching","volume":"25","author":"Guo","year":"2010","journal-title":"J Comput Sci Technol"},{"issue":"4","key":"10.3233\/JIFS-179502_ref2","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/s10009-014-0307-4","article-title":"Automated verification of the FreeRTOS scheduler in Hip\/Sleek[J]","volume":"16","author":"Ferreira","year":"2014","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.3233\/JIFS-179502_ref3","doi-asserted-by":"crossref","unstructured":"Wu S. , A Traffic Motion Object Extraction Algorithm, International Journal of Bifurcation and Chaos 25(14) (2015), Article Number 1540039.","DOI":"10.1142\/S0218127415400398"},{"key":"10.3233\/JIFS-179502_ref4","doi-asserted-by":"crossref","first-page":"598","DOI":"10.1016\/j.future.2018.04.040","article-title":"Research on internet information mining based on agent algorithm","volume":"86","author":"Wu","year":"2018","journal-title":"Future Generation Computer Systems"},{"key":"10.3233\/JIFS-179502_ref5","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1016\/j.cogsys.2018.07.035","article-title":"Bidirectional cognitive computing method supported by cloud technology","volume":"52","author":"Wu","year":"2018","journal-title":"Cognitive Systems Research"},{"key":"10.3233\/JIFS-179502_ref6","first-page":"16","article-title":"Towards verified virtual memory in L4[J]","volume":"4","author":"Klein","year":"2004","journal-title":"TPHOLs Emerging Trends"},{"key":"10.3233\/JIFS-179502_ref7","first-page":"207","article-title":"Verified Correctness and Security of OpenSSL HMAC[C]\/\/","author":"Beringer","year":"2015","journal-title":"24th USENIX Security Symposium (USENIX Security 15)"},{"issue":"1-4","key":"10.3233\/JIFS-179502_ref8","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","article-title":"VST-Floyd: A separation logic tool to verify correctness of C programs","volume":"61","author":"Cao","year":"2018","journal-title":"J Autom Reasoning"},{"key":"10.3233\/JIFS-179502_ref9","first-page":"53","article-title":"The CompCert verified compiler[J]","author":"Leroy","year":"2012","journal-title":"Documentation and user\u2019s manual. INRIA Paris-Rocquencourt"},{"issue":"3","key":"10.3233\/JIFS-179502_ref10","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","article-title":"Mechanized semantics for the Clight subset of the C language[J]","volume":"43","author":"Blazy","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/JIFS-179502_ref11","first-page":"332","article-title":"Formal methods for component software: The refinement calculus perspective[C]\/\/European Conference on Object-Oriented Programming. Springer","author":"B\u00fcchi","year":"1997","journal-title":"Berlin, Heidelberg"},{"issue":"2","key":"10.3233\/JIFS-179502_ref12","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/s10270-014-0410-8","article-title":"Component-based verification using incremental design and invariants[J]","volume":"15","author":"Bensalem","year":"2016","journal-title":"Software & Systems Modeling"},{"issue":"1","key":"10.3233\/JIFS-179502_ref13","first-page":"595","article-title":"Deep specifications and certified abstraction layers[C]\/\/ACM SIGPLAN Notices","volume":"50","author":"Gu","year":"2015","journal-title":"ACM"}],"container-title":["Journal of Intelligent & Fuzzy Systems"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JIFS-179502","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T13:59:17Z","timestamp":1732629557000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress&doi=10.3233\/JIFS-179502"}},"subtitle":[],"editor":[{"given":"Mohamed","family":"Elhoseny","sequence":"additional","affiliation":[]},{"given":"X.","family":"Yuan","sequence":"additional","affiliation":[]}],"short-title":[],"issued":{"date-parts":[[2020,2,6]]},"references-count":13,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.3233\/jifs-179502","relation":{},"ISSN":["1064-1246","1875-8967"],"issn-type":[{"type":"print","value":"1064-1246"},{"type":"electronic","value":"1875-8967"}],"subject":[],"published":{"date-parts":[[2020,2,6]]}}}