@article{(Open Science Index):https://publications.waset.org/pdf/8630, title = {Application of Formal Methods for Designing a Separation Kernel for Embedded Systems}, author = {Kei Kawamorita and Ryouta Kasahara and Yuuki Mochizuki and Kenichiro Noguchi}, country = {}, institution = {}, abstract = {A separation-kernel-based operating system (OS) has been designed for use in secure embedded systems by applying formal methods to the design of the separation-kernel part. The separation kernel is a small OS kernel that provides an abstract distributed environment on a single CPU. The design of the separation kernel was verified using two formal methods, the B method and the Spin model checker. A newly designed semi-formal method, the extended state transition method, was also applied. An OS comprising the separation-kernel part and additional OS services on top of the separation kernel was prototyped on the Intel IA-32 architecture. Developing and testing of a prototype embedded application, a point-of-sale application, on the prototype OS demonstrated that the proposed architecture and the use of formal methods to design its kernel part are effective for achieving a secure embedded system having a high-assurance separation kernel. }, journal = {International Journal of Computer and Information Engineering}, volume = {4}, number = {8}, year = {2010}, pages = {1349 - 1357}, ee = {https://publications.waset.org/pdf/8630}, url = {https://publications.waset.org/vol/44}, bibsource = {https://publications.waset.org/}, issn = {eISSN: 1307-6892}, publisher = {World Academy of Science, Engineering and Technology}, index = {Open Science Index 44, 2010}, }