As become more widely used, embedded systems security has increasingly gained attention. From the hardware point
of view, this paper describes the background of approach to the vulnerabilities and hardware Trojan detection of
embedded system, basic ideas and objectives; established the model- ESM (Embedded Systems Model) used to describe
embedded systems, provides the encoding method of the ESM system state. Based on this model, this article describes
how to use model checking methods to detect vulnerabilities and Trojan existence of an embedded system.