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
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;
Conference_Titel :
Consumer Electronics (GCCE), 2014 IEEE 3rd Global Conference on
Conference_Location :
Tokyo
DOI :
10.1109/GCCE.2014.7031136
