Formal Method B And Factor In The Network Modeling Application

In the highly-credible software engineering, the formal method has been used to ensure the validity and consistence in the development of the software. B, VDM and Z are formal methods based on the construction of models. B is produced on the basis of the VDM and Z. Because some of its notable advantages coupled with the support of robust tools, the successful application of the B method and language to large industrial system ,in a range of technical areas: real-time, simulation, information processing and engineering.B is a short name of B techniques,methods and tools. B (composed of B method, B tools and B toolkits)is a robust practice-oriented software process technique which is based on the theory of mathematics. The notions and methods which B used support most software process: the requirements analysis,the specification,designing of software,implement and maintenance. Layered software structure gradually along with the gradual recognition and validation is the guiding principle of B method. B toolkits including a large number of tools, all the tools is integrated in a Windows-based software development environment. These tools can be integrated automatically, and therefore it can support the B method to develop software in the entire software development process. B tools support the progressive structure of the software, the confirmation process can be static analysis and dynamic analysis using simulation techniques, the integrated theorem prover can be used for the validity proveness.UML applied to the software development methodology, software life-cycle stages, various application fields and the various development tools, UML is a summary of previous modeling experience and absorb the outstanding achievements of today's standard model. Exact Software Requirements is the software quality assurance, UML plays an important role in software demand. It is used to describe software demand model, object model, the dynamic model and the deployment model. However, UML is lack of accurate semantic of formal methods, it is difficult to have accurate ambiguity software statute. I proposes a combination of B and the use of the UML, using formal methods to generate accurate semantic accuracy statute of the same system. B language can provide a lively and rigorous certification, Therefore the combination of UML-B can create a formal precision of UML, and produce the behavior model on the basis of refinement and Object-oriented.Cytokine network is a interesting research, but it is also a difficult. On one hand, a few persons do much study in this aspect and get much research results,but it still exists much problem. Although in these results it discover many cytokines and they carried on deep research on its function, it can't definitely ensure the function of cytokine, only knows the biological function of this cytokine and its function result, it is not enough for us to study the cytokine network. On the other hand, with the computer technical development, the computer has already become a very useful assistance tool of all fields, why do not use the way of computer to simulate the cytokine's function, from which we can discover its regulation.In our work, we use the B method to build up cytokine network of formal model. Based on this model, we can use computer program certification from the College of Animal Sciences and in the experimental data if is correct, And let us compare the dynamic behavior of the model and experimental results whether are matched. Research shows :because of the complexity of biology, it is impossible for us to simply rely on the experimental equipment to fully understand the biology.Formal method B is one of a few formal software development methodology. It is based on strict mathematical basis, throughout the software development process, it is particularly suitable for complex system development. Rigorous mathematical test to ensure every step is correct. In my work, I tested the abstract machine of the complex cytokine network, ensuring the correctness of the abstract machine.The B method is one of the most popular formal methods at present, and people write the software system specification with B method, and carry on the system design and description. The B method has already been used in some very important software items and acquired successful. in the biology ,there are a few successful examples , so I modeled the cytokine network with B.