论文部分内容阅读
场景是一种分析与验证需求的有效工具,因此基于场景的分析与设计受到广泛关注。一个系统需求由多个局部场景构成,这些场景是由不同的相关人员根据自己所关注的业务功能并结合自己的知识给出,每个场景描述系统中不同用户的需求,多个场景所描述的用户需求可能存在某些业务需求的重叠,局部场景中可能含有不确定行为,如何对含有不确定行为的场景进行建模和分析,以及如何把从这些局部场景中抽取的行为模型合并(merge)成一个完整的系统行为模型是本文研究的重点。文中所说的合并不同于行为模型的并行复合(parallel composition),并行复合主要针对不同构件系统的行为组合,而行为模型的合并是从同一构件系统的两个局部行为模型中获得一个精化的模型。范畴论是一种抽象的数学理论,集中关注对象之间的关系和交互作用,把态射看作是保持系统结构的一种映射,它可以确定对象(行为模型)之间的交互本质。因此本文使用范畴论的方法研究行为模型之间的交互关系,以便进行行为模型的合并。本文采用模态迁移系统描述系统行为,针对局部行为模型中存在的不确定行为,提出一种基于事件轨迹的合并方法。文中首先给出了模态迁移系统的形式化方法,因为模态迁移系统描述事件的迁移关系,不利于研究行为模型整体之间的关系,所以本文使用基于事件轨迹集的合并方法。本文首先根据MTS的路径构造了相应的事件轨迹,并给出了MTS模型的事件轨迹集。并在MTS范畴和Trc范畴之间定义了两个函子,通过自然变换得出重要结论:事件轨迹集范畴保留模态迁移系统范畴的精化关系,因此我们研究模态迁移系统的合并可以通过研究事件轨迹集的合并来实现。我们知道事件轨迹集的合并就是为了把模型的可能轨迹变成必然轨迹,或者删除一些不可能发生的可能轨迹,也就是得到一个精化轨迹集,因此在研究事件轨迹集的合并之前,首先定义了事件轨迹集的精化轨迹集。并根据事件轨迹集的精化程度给出了最小共同精化和极小共同精化。事件轨迹集的合并是为了得到一个最小共同精化,但是经研究分析发现有些事件轨迹集的最小共同精化不一定存在,而极小共同精化又不唯一,如果合并只是得到极小共同精化其中一个,就排除了其他极小共同精化存在的可能性,针对这种情况,我们给出最大共同抽象的概念,也就是所有极小共同精化的一个下确界。同时我们还研究了最小共同精化存在的必要条件即确定条件和多重可能条件。在合并方法上,根据事件轨迹集之间的关系的不同,并结合范畴的泛构造的特点,给出两种范畴的泛构造方法即和(余积)与推出,用于事件轨迹集的合并。文中还讨论了事件轨迹集合并与精化规则,最后利用余极限讨论了多个事件轨迹集合并。