Research And Application On Verification Technology Of Formal B Method

The B-method is a well-established theory and methodology for the rigorous development of computer systems. It is useful and right to the description of the large and complicated system particularly. It is a method of detailed description,the design and complex system encoding. Through the B-method, the description and certification can help find the inconsistencies, not clear and incomplete in the system description that other ways not easy to find. Software developers will be helped to increase the understanding of the systems. The experience in the process of the system design tells us that the bottleneck is the verification and confirmation.Verification of formal method include theorem proving and model checking.Theorem proving is a method that uses the reasoning rules to deduce the expectations of the characteristics. Deductions rely on the the rules and reasoning. In the thesis the machines of cytokine network uesing B method is verificated, which ensure the machine exact.Today,model checking is one of the most important fomal verifieation methods. It is widely employed to verify software and hardware systems. Model checking searches the finited state spaces exhaustively. The main method of model checking is using formal description language or the transition form system to model the systems. And then do its verification automately. It allows developer verificate the state space all throurgh the machines. Using the algorithm in finite steps automatic detect the system whether or not to be satisfied the nature. The main shortcomings of model checking are state-space explosion. The state-space explosion has been reformed, because of the non-deterministic of the systems, when the number of mutual communication subsystems incresed, the whole system will also increase. On the other hand, the system contains great data, the different combinations will produce more states. The combination of subsystems or a combination of data domains, will leads the whole state-spaces grown exponentially. This thesis presents the application of conditions analysis to solve the problem of state-space explosion, which consider the relationship inputs and outputs to delete the state-space.Refinement is a key concept in the B-Method. It allows one to start from a high-level specification and then gradually refine it into an implementation, which can then be automatically translated into executable code. The model refinement can be refined until they contain sufficient implementation details. The model refinement guarantees that, during successive refinements of the abstract machines, every invariant and precondition defined will be fulfilled. The operations, the invariants and the preconditions produce a set of proof obligations that must be formally proven every time a system model is enriched with additional design details. The last refinement of a machine is called implementation. In this thesis, the machines of the cytokine network models are refined, which is less non-determinism and more concretely. In the last, we give code implementation of the cytokine network.