Merging Research On Partial Behavioral Models

Requirement analysis for software engineering is the process to establish the models of synergizing information, functions and system behaviors by understanding and analyzing the to-be solved problems and the relevant environment, and then make the customer needs precise and complete so as to eventually form the requirement specification; while the Formal Methods applied for requirement analysis are base on the rigorous mathematic theory and to solve the problem of "what to do" of the target system through mathematic methods manually.Model transition system, as the formal model-establishing method base on state machine, is widely used for formal description of the system behavior. This method often assumes the behavior of the target system has been described completely in a certain way. This assumption is effective to some extent if the attribute is clear and well-known; while it can't meet the requirements at the beginning stage of the model-establishing for the system behavior; thus the information required in the requirements elicitation process needs to be perfect step by step. To obtain the more accurate and complete requirements specification of the target system, this essay defines how the partial modal transition systems to describe the partial behavior of the target system more accurately through extending modal transition systems. The partial modal transition system provide related formal requirements specification for the enabled, uncertain and proscribed behaviors of the described customer requirements; and the other behaviors non-described behaviors are regarded as unrelated and undefined behaviors since it exceeds those ranges focused and cared by particular customers.To eliminate the undefined behaviors existing in partial behavior model and obtain the global behavior model, the essay proposes a merging method for the partial behavior model base on event and status, which defines the refinement relationship between the models and finally acknowledge the more certain model through comparing the refinement relationship; moreover it provides evident to fix the right models we expect. Since we often hope the merging model can't input additional requirement information, the merging process is that of least common refinement (minimal common refinement) to establish the original model. The basis of our algorithms is the operator+u & +1, the user can work out the upper bounds and lower bounds for the merging model. And the model establisher can also selectively get the expected minimal common refinement through further refining to the upper bounds. Furthermore; by merging all the partial behavior model of the target system and consistently exchanging with the related customers during the merging process, it can refine the uncertain behavior existing in the model and finally achieve the enabled behavior model which only include the partial labelled transition systems model for inevitable transition and proscribed transition, and make the implementation of the original models we expected as well; that is partial labelled transition system model...