Model Checking of Embedded Assembly Program Based on Simulation
Satoshi Yamane, Ryosuke Konoshita, Tomonori Kato · IEICE Transactions on Information and Systems · 2017
Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking. In addition, we have introduced undefined values to reduce the number of states in order to avoid the state space explosion.