Formal Study Of Neuroendocrine Complex System

At present, the software industrial community faces with pressure: the function of the software products becomes more and more complex. The aim of software engineering is that we can still produce correct and reliable system when the complexity of the software is increased. Formal method is one of the ways to achieve the goal. Formal method is efficient way, which is used for requirement analyzing, designing and validating during developing of software systems. It is based on mathematics, and includes various languages, techniques and tools.The requirement elicitation is the most difficult and important part in the software development. The existing requirement elicitation method is available such as interview, questionnaire, observation and user data research and so on. These are simple methods. However, these methods can cause many errors, especially for complex systems. Therefore, this thesis suggests use the complex networks as a method of requirement elicitation. Complex networks can describe variety different practical systems. It may serve as a useful tool for understanding complex systems.After the requirement acquisition of the complex system using complex network, then describe these using formal methods to improve the reliability of the system. But B method is object-oriented, but not object-based and readability of requirements specification is poor. Poor readability prevents user involvement in the validation of these specifications. The Unified Modeling Language (UML) has become a defac to standard notation for describing analysis and design models of object-oriented software systems. But UML is lack of rigorous semantics, so it is difficult to verify and analyze UML specifications. This point is considered as a serious drawback of UML-based technique.In view of the above questions, this thesis proposes thought of formal B method transferring to UML. It also integrates formal B method and UML to model software systems. Among them, B method is used as mathematical foundation, UML is used as a language for modeling, and the graphical description of models is easily accessible. The study of formal semantics transition of UML can enhance the accuracy, consistency and expansibility of this language. Then we can provide a theoretical method for the validation, transition and consistency checking of the model.In this thesis, we do the following work:1,We conclude the existing method of requirement elicitation, proposed degree relevant characteristics of complex networks as requirement elicitation.2,We study the neuroendocrine system using complex networks, acquire the main properties of the system and important cells and meditors.3,Describe the system with formal B methods by the complex network characteristics, give animation and model checking based on the resulted formal models using of ProB.4,Provide improved conversion method of B to the UML class diagram, overcome the original method that can not transform the dynamic part of the machine and has other shortcomings.This thesis use the complex networks as a method of requirement elicitation, and proposed the improved conversion method of B to the UML class diagram. Neuroendocrine system is our application research. Using improved conversion method of B to the UML class diagram, we can get the class diagrams, and implement.