%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