Title :
Verifying Behavior of L4 Microkernel based Mobile Phone
Author :
Bang, Ki-Seok ; Lee, Su-Young ; Nam, Ki-Hyuk ; Lee, Wan-Yeon ; Ko, Young-Woong
Author_Institution :
Coll. of Inf. & Electron. Eng., Hallym Univ., Chunchon
Abstract :
The embedded mobile phone based on L4 microkernel are known to be difficult to predict their behavioral correctness since L4 microkernel communicates with various components for their execution. That means its correctness is not easy to guarantee by using traditional design and testing methods. In this paper, we propose a formal approach to prove the correctness of L4 based mobile platforms.
Keywords :
mobile handsets; operating system kernels; telecommunication computing; L4 based mobile platforms; L4 microkernel based mobile phone; behavioral correctness; Embedded system; Formal verification; GSM; Ground penetrating radar; Mobile handsets; Modems; Multiaccess communication; Operating systems; Software systems; System recovery; Formal Verification; IPC mechanism; L4 Microkernel; Model Checking; Operating System; SPIN; SyncChart;
Conference_Titel :
Advanced Communication Technology, The 9th International Conference on
Conference_Location :
Gangwon-Do
Print_ISBN :
978-89-5519-131-8
DOI :
10.1109/ICACT.2007.358317
