Combination of Model Checking and Theorem Proving to Verify Embedded Software

In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software.