Propositional modal logic is the logic studying the necessity,possibility and their correlated concepts. The satisfiability problem of model formula and the proof of system completeness problem are two classic problems in modal logic. To solve these two problems, we propose a method of canonical model to construct the modal formula. By this method,for a given model formula phi, if phi is satisfiable,a canonical model can be obtained for it ; but if phi is not satisfiable,a proof of its negation- phi is to be obtained. In addition,in the paper we also give a constructive proof method of the completeness of the propositional modal logic.
