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).
montao / formal-verification Goto Github PK
View Code? Open in Web Editor NEW๐ The SMV models
License: BSD 2-Clause "Simplified" License