The Study About Formal Validation Of Causal Behaviors Of Domains In Problem Frames

In recent years, with the rapid development of computer industry, the scale of software and information technology services industry continues to expand, the complexity continues to increase, part of the software products in the R&D process because of financial, human and other causes of the project behind schedule, software quality can not meet the design requirements, gradually from the previous requirement. From the perspective of software engineering, software project success or failure is the main cause of the demand, the quality of demand analysis is of great significance to the quality of the final software product. Especially in safety critical (Safety-Critical) of major scientific research projects, the requirements analysis directly affects the progress and development of quality projects, demand failure or incomplete work will not only delay the progress of the project, it may cause unpredictable losses to the entire project. Therefore, in the actual project development process, we should face up to the requirement analysis of the system, to ensure the integrity of the demand analysis.As a method of requirement analysis, the theory of Problem Frames emphasizes the role of the real world of the software system,make requirement transformated by constructing a context diagram, graph, using the progression of problem in fields,to acheive a smooth deduction transformation of user requirements to software specification. However, the gradual realization of modeling and the problems based on the Problem Frames of methods mainly depend on the demand the analyst’s intuition and experience, which limits the demand analysis to a certain extent the rigor and traceability, especially in the analysis of safety critical software system requirements, ask questions model plays a key role in the field of if there is the desired state unreachable or ill structured problems, the correctness of the protocol by means of the software can not be guaranteed, the lack of formal evidence and argument. Therefore, the problem in the field of formal verification of transfer model between business systems especially the acquisition has important theoretical significance and practical application value and processing software specification of safety critical systems. Model checking is a formal verification method and other verification techniques or methods have many advantages compared to the most important, is the high degree of automation, the system can automatically check the finite state space structure, and the system specification description was improved. As a branch of model checking, the method of symbolic model checking not only inherits the characteristics of high degree of automation of the model test, at the same time, to a certain extent to avoid the state explosion problem, the scale of the problem solving can also increase. The method is verified by a series of Boolean expressions to express the relationship between the transfer system of all States and between States, the Boolean expression to determine the compression storage method in figure OBDD (Ordered Binary Decision ordered two fork in Diagram).In this paper, the theory of Problem Frame and symbolic model checking based on, it puts forward a set of state transition model of the relationship between critical domains in the field of verification method, implicit mapping out the corresponding external sharing rules and internal state change events, so as to determine the external field is shared between the causal relationship between the phenomena, and provide reliable guarantee for the realization of the problem the gradient. At the same time, by combining the frame theory and symbolic model checking method, through the model checking to determine the form of basis transform causal relationship and problems progression; the definition of the Kripke structure and the UML state machine set of mapping rules from one to another, the UML state machine to convert the input language of verification tools for the form, through the verification reachability properties determine the migration path, and screened with the causal relationship between events, support gradient.