{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:10:02Z","timestamp":1748412602169,"version":"3.41.0"},"reference-count":25,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2015]]},"DOI":"10.1587\/transinf.2014fop0004","type":"journal-article","created":{"date-parts":[[2015,5,31]],"date-time":"2015-05-31T22:10:06Z","timestamp":1433110206000},"page":"1137-1149","source":"Crossref","is-referenced-by-count":1,"title":["A Framework for Verifying the Conformance of Design to Its Formal Specifications"],"prefix":"10.1587","volume":"E98.D","author":[{"given":"Dieu-Huong","family":"VU","sequence":"first","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"CHIBA","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenro","family":"YATAKE","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshiaki","family":"AOKI","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] J.R. Abrial, Modeling in Event-B: System and software engineering, Cambridge University Press, 2010.","DOI":"10.1017\/CBO9781139195881"},{"key":"2","doi-asserted-by":"crossref","unstructured":"[2] T. Aoki, \u201cModel checking multi-task software on real-time operating systems,\u201d 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing, pp.551-555, 2008.","DOI":"10.1109\/ISORC.2008.46"},{"key":"3","unstructured":"[3] C. Baier and J.P. Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 2008."},{"key":"4","unstructured":"[4] D. Bert, M.L. Potet, and N. Stouls, \u201cGenesyst: A tool to reason about behavioral aspects of B Event specifications. Application to security properties,\u201d CoRR, vol.abs\/1004.1472, 2010."},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] P. Bostrom, \u201cCreating sequential programs from Event-B models,\u201d Proc. 8th International Conference on Integrated Formal Methods, IFM '10, Berlin, Heidelberg, pp.74-88, 2010.","DOI":"10.1007\/978-3-642-16265-7_7"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] P.J. Broadfoot and A.W. Roscoe, \u201cTutorial on FDR and its applications,\u201d Proc. 7th International SPIN Workshop, pp.322-322, 2000.","DOI":"10.1007\/10722468_18"},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] Y. Choi, \u201cModel checking trampoline OS: A case study on safety analysis for automotive software,\u201d Softw. Test., Verif. Reliab., vol.24, no.1, pp.38-60, 2014.","DOI":"10.1002\/stvr.1482"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, \u201cPatterns in property specifications for finite-state verification,\u201d Proc. 21st International Conference on Software Engineering, ICSE '99, pp.411-420, 1999.","DOI":"10.1145\/302405.302672"},{"key":"9","unstructured":"[9] G.J. Holzmann, The SPIN Model Checker-primer and reference manual, Addison-Wesley, 2004."},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] T. In der Rieden and S. Knapp, \u201cAn approach to the pervasive formal specification and verification of an automotive system: Status report,\u201d Proc. 10th International Workshop on Formal Methods for Industrial Critical Systems, FMICS '05, pp.115-124, 2005.","DOI":"10.1145\/1081180.1081195"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, \u201cseL4: Formal verification of an operating-system kernel,\u201d Commun. ACM, vol.53, no.6, pp.107-115, 2010.","DOI":"10.1145\/1743546.1743574"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] M. Leuschel and M. Butler, \u201cProB: An automated analysis toolset for the B method,\u201d Int. J. Software Tools for Technology Transfer, vol.10, no.2, pp.185-203, 2008.","DOI":"10.1007\/s10009-007-0063-9"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] N. Lynch and F. Vaandrager, \u201cForward and backward simulations: Untimed systems,\u201d Inf. Comput., vol.121, no.2, pp.214-233, Sept. 1995.","DOI":"10.1006\/inco.1995.1134"},{"key":"14","unstructured":"[14] P. Matos, B. Fischer, and J. Marques-Silva, \u201cA lazy unbounded model checker for Event-B,\u201d Formal Methods and Software Engineering, Lect. Notes Comput. Sci., vol.5885, pp.485-503, 2009."},{"key":"15","unstructured":"[15] R. Milner, Communication and concurrency, PHI Series in Computer Science, Prentice Hall, 1989."},{"key":"16","unstructured":"[16] A. Muller, \u201cVDM-the vienna development method,\u201d Bachelor thesis in Formal Methods in Software Engineering, Johannes Kepler University Linz, 2009."},{"key":"17","unstructured":"[17] T. Muller, \u201cFormal methods, model-cheking and rodin plugin devel-opment to link Event-B and Spin,\u201d IEICE Technical Report, SS., vol.109, no.170, pp.43-48, 2009."},{"key":"18","doi-asserted-by":"crossref","unstructured":"[18] G. O'Regan, \u201cZ formal specification language,\u201d in Mathematics in Computing, pp.109-122, Springer London, 2013.","DOI":"10.1007\/978-1-4471-4534-9_6"},{"key":"19","unstructured":"[19] OSEK\/VDX Group, \u201cOSEK\/VDX operating system specification 2.2.3, http:\/\/portal.osek-vdx.org\/.\u201d"},{"key":"20","doi-asserted-by":"crossref","unstructured":"[20] S. Reeves and D. Streader, \u201cGuarded operations, refinement and simulation,\u201d Electron. Notes Theor. Comput. Sci., vol.259, pp.177-191, 2009.","DOI":"10.1016\/j.entcs.2009.12.024"},{"key":"21","unstructured":"[21] J. Rumbaugh, I. Jacobson, and G. Booch, Unified Modeling Language Reference Manual, 2nd ed., Pearson Higher Education, 2004."},{"key":"22","unstructured":"[22] M.Y. Vardi and P. Wolper, \u201cAn automata-theoretic approach to automatic program verification,\u201d Proc. 1st Annual Symposium on Logic in Computer Science (LICS '86), pp.332-344, 1986."},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] D.H. Vu and T. Aoki, \u201cFaithfully formalizing OSEK\/VDX operating system specification,\u201d Proc. 3rd Symposium on Information and Communication Technology, pp.13-20, 2012.","DOI":"10.1145\/2350716.2350721"},{"key":"24","unstructured":"[24] D.H. Vu, Y. Chiba, K. Yatake, and T. Aoki, \u201cChecking conformance of a Promela design to its formal specification in Event-B,\u201d Preliminary proceeding of the third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), pp.188-203, 2014."},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] K. Yatake and T. Aoki, \u201cModel checking of OSEK\/VDX OS design model based on environment modeling,\u201d Proc. 9th International Colloquium on Theoretical Aspects of Computing (ICTAC '12), pp.183-197, 2012.","DOI":"10.1007\/978-3-642-32943-2_15"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E98.D\/6\/E98.D_2014FOP0004\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T05:32:00Z","timestamp":1748410320000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E98.D\/6\/E98.D_2014FOP0004\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2014fop0004","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"type":"print","value":"0916-8532"},{"type":"electronic","value":"1745-1361"}],"subject":[],"published":{"date-parts":[[2015]]}}}