Abstract: A strategy of combining Model checking and theorem proving techniques to develop and verify high confidence embedded software was proposed. First, the UML state machine of software model was transformed into the input modeling language of model checker MOCHA and the model was analyzed in the model checking tool with associated property specifications expressed in temporal logic. The model checker can give counterexamples if it decided that the model can not satisfy any of the specified properties, which can be used to modify the software`s UML design model. The UML model which has been verified by MOCHA was then transformed into abstract specifications of theorem prover Atelier-B, in which the model would be refined, verified and translated into source C code. The transformation rules from UML state machine to REACTIVE MODULES and to B abstract machines were given. The experiment showed that the proposed strategy can effectively improve the development and verification of high-confidence embedded software.