• DocumentCode
    256786
  • Title

    Model generation by the exhaustive search for embedded assembly programs and application to model checking

  • Author

    Konoshita, R. ; Sakurai, K. ; Yamane, S.

  • Author_Institution
    Grad. Sch. of Natural Sci. Technol., Kanazawa Univ., Kanazawa, Japan
  • fYear
    2014
  • fDate
    7-10 Oct. 2014
  • Firstpage
    699
  • Lastpage
    702
  • Abstract
    Embedded systems have been widely used. Therefore, it is important to ensure the safety. Model checking is effective to ensure the safety for systems. We have developed Behavior Extractor to model the behavior of embedded assembly programs automatically. The model is used for model checking. In addition, we have introduced the undefined value to reduce the number of states.
  • Keywords
    embedded systems; program verification; behavior extractor; embedded assembly programs; embedded systems; exhaustive search; model checking; model generation; Assembly; Clocks; Educational institutions; Light emitting diodes; Model checking; Registers; Sensors;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Consumer Electronics (GCCE), 2014 IEEE 3rd Global Conference on
  • Conference_Location
    Tokyo
  • Type

    conf

  • DOI
    10.1109/GCCE.2014.7031136
  • Filename
    7031136
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=256786