| With the development of modern science and technology, the power distribution automation domain has obtained the rapid development. Although many research results have been gained, some problems still exist. Now, The present power distribution automated system is unable to carry on the strict inspection, its code accuracy only can depend upon the test, but it can't prove that the software does not have the mistake. The formalized methods may solve this kind of problem effectively. B method is a kind of them, which is a software exploitation method based on rigorous mathematics. It provides a unified mathematics frame, through a series of proof duty, and it can prove the accuracy of the system structure, then the realization system has the high security and reliability.In view of the above situation, this article has mainly done following work:1. The paper introduces the present research situation of B method, and has made a more thorough study to the correlation theories of B method. And it mainly includes the mathematics knowledge, each stage of developing the software, the certification technology, as well as the comparative analysis of B tool and so on.2. The system model has designed, and the model extraction has carried on according to characteristics of the system. The real number abstract machine, the plural number abstract machine, the node abstract machine, the electric current monitor and the central controller with the B method has been constructed. And simultaneously partial the abstract machines were to carry on the purification and the realization. Because of the uncertainly of FTU, the paper increases PB.3. Take REAL_TYPE and CONTROLLER machines for example, some proof of correctness has been done, and some experimental results have been gotten. The paper points out some problems to be improved during the next work. |