Our aim has been to build and verify SMV models of hardware peripherals with use of the model checker NuSMV to check security properties and a liveness property. We created a model of the CPU, a model of the universal asynchronous transmitter/receiver (UART), a DMA controller model, an MMU model and a model of the main memory (RAM).