• DocumentCode
    462940
  • 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
  • Volume
    1
  • fYear
    2007
  • fDate
    12-14 Feb. 2007
  • Firstpage
    113
  • Lastpage
    115
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Advanced Communication Technology, The 9th International Conference on
  • Conference_Location
    Gangwon-Do
  • ISSN
    1738-9445
  • Print_ISBN
    978-89-5519-131-8
  • Type

    conf

  • DOI
    10.1109/ICACT.2007.358317
  • Filename
    4195096
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=462940