%0 Journal Article %A Kei Kawamorita and Ryouta Kasahara and Yuuki Mochizuki and Kenichiro Noguchi %D 2010 %J International Journal of Computer and Information Engineering %B World Academy of Science, Engineering and Technology %I Open Science Index 44, 2010 %T Application of Formal Methods for Designing a Separation Kernel for Embedded Systems %U https://publications.waset.org/pdf/8630 %V 44 %X 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. %P 1349 - 1357