Trace-based Merging Of Partial Beahavioral Models

The scenarios widely recognized as an effective ways for requirements elicitation, documentation and certification, and they support a formal, informal, narrative and concrete style description, and they also concerns the dynamic characteristics of interactive software environment. Scenarios are typically provided by different stakeholders with different viewpoints, describing different, yet overlapping aspects of the same system. There are unknown behaviours in the scenarios. How should describe system behavioral and these partial models be put together?Composition of behavioural models is an old idea; however, its main focus has been on parallel composition which describes how two different components work together. In the context of model elaboration, what we are interested in is composing two partial descriptions of the same component to obtain a more elaborate version of both original partial descriptions. We call this operation a merge.A distinctive attribute of category theory as a mathematical formalism is that it is essentially graphical. This means that most concepts and properties can be defined, proved and/or reasoned about using diagrams of a formal nature. Therefore, we study relation and mergeing between behavioral models with category theory.System behavioral is described by modal transition systems. In allusion to unknown behavioral in partial behavioral models, we formally define model merging based on event trace. First, we give formal definition of modal transition system. Main focus of modal transition system is transition relations between states, which is not conducive to study the relationship of behavior models, so we propose merge method based on trace. The first problem is how to construct the set of event traces of modal transition system. We construct traces according to paths of modal transition system and formally define the traces set. With natural transformations and two functors between the category MTS and category Trc, a very important conclusion:since the category Trc retains refinement relation of the category MTS, studing the merge of the trace sets replace studing merge of modal transition system.Refinement of the traces captures the notion of elaboration of a partial.description into a more comprehensive one, in which some knowledge over the maybe trace has been gained. It can be seen as being a "more defined than" relation between two partial models. Merging of the traces is to convert maybe traces into required traces or remove them altogether. We formally define least common refinement and minimal common refinement. The merge of the traces cannot be defined as their least common refinement, because it is possible that there is no common refinement, or a common refinement exists, but there is no least one. There is more than one minimal common refinement. However, any choice of minimal common refinement rules out the others. Hence, it is helpful to find a set of trace that characterizes the point in which incompatible decisions must be made in order to merge two sets of traces and produce a minimal common refinement. This set of traces is the greatest lower bound (glb) of all minimal comfimon refinements. We also discuss necessary conditions for the existence of least common refinement, i.e. determinacy condition and multiple-maybe condition.According to different relations between sets of traces and characteristics of the category constructions, we propose two universal constructions as a general solution to merging. Last, we use colimit to discuss merging of multiple sets of traces.