基于事件軌跡的局部行為模型的合并.pdf

1、場景是一種分析與驗證需求的有效工具,因此基于場景的分析與設(shè)計受到廣泛關(guān)注。一個系統(tǒng)需求由多個局部場景構(gòu)成,這些場景是由不同的相關(guān)人員根據(jù)自己所關(guān)注的業(yè)務(wù)功能并結(jié)合自己的知識給出,每個場景描述系統(tǒng)中不同用戶的需求,多個場景所描述的用戶需求可能存在某些業(yè)務(wù)需求的重疊,局部場景中可能含有不確定行為,如何對含有不確定行為的場景進(jìn)行建模和分析,以及如何把從這些局部場景中抽取的行為模型合并(merge)成一個完整的系統(tǒng)行為模型是本文研究的重點。文中

2、所說的合并不同于行為模型的并行復(fù)合(parallelcomposition),并行復(fù)合主要針對不同構(gòu)件系統(tǒng)的行為組合,而行為模型的合并是從同一構(gòu)件系統(tǒng)的兩個局部行為模型中獲得一個精化的模型。
　　 范疇論是一種抽象的數(shù)學(xué)理論,集中關(guān)注對象之間的關(guān)系和交互作用,把態(tài)射看作是保持系統(tǒng)結(jié)構(gòu)的一種映射,它可以確定對象(行為模型)之間的交互本質(zhì)。因此本文使用范疇論的方法研究行為模型之間的交互關(guān)系,以便進(jìn)行行為模型的合并。
　　 本

3、文采用模態(tài)遷移系統(tǒng)描述系統(tǒng)行為,針對局部行為模型中存在的不確定行為,提出一種基于事件軌跡的合并方法。文中首先給出了模態(tài)遷移系統(tǒng)的形式化方法,因為模態(tài)遷移系統(tǒng)描述事件的遷移關(guān)系,不利于研究行為模型整體之間的關(guān)系,所以本文使用基于事件軌跡集的合并方法。本文首先根據(jù)MTS的路徑構(gòu)造了相應(yīng)的事件軌跡,并給出了MTS模型的事件軌跡集。并在MTS范疇和Trc范疇之間定義了兩個函子,通過自然變換得出重要結(jié)論:事件軌跡集范疇保留模態(tài)遷移系統(tǒng)范疇的精化關(guān)

4、系,因此我們研究模態(tài)遷移系統(tǒng)的合并可以通過研究事件軌跡集的合并來實現(xiàn)。
　　 我們知道事件軌跡集的合并就是為了把模型的可能軌跡變成必然軌跡,或者刪除一些不可能發(fā)生的可能軌跡,也就是得到一個精化軌跡集,因此在研究事件軌跡集的合并之前,首先定義了事件軌跡集的精化軌跡集。并根據(jù)事件軌跡集的精化程度給出了最小共同精化和極小共同精化。事件軌跡集的合并是為了得到一個最小共同精化,但是經(jīng)研究分析發(fā)現(xiàn)有些事件軌跡集的最小共同精化不一定存在,而極

5、小共同精化又不唯一,如果合并只是得到極小共同精化其中一個,就排除了其他極小共同精化存在的可能性,針對這種情況,我們給出最大共同抽象的概念,也就是所有極小共同精化的一個下確界。同時我們還研究了最小共同精化存在的必要條件即確定條件和多重可能條件。
　　 在合并方法上,根據(jù)事件軌跡集之間的關(guān)系的不同,并結(jié)合范疇的泛構(gòu)造的特點,給出兩種范疇的泛構(gòu)造方法即和(余積)與推出,用于事件軌跡集的合并。文中還討論了事件軌跡集合并與精化規(guī)則,最后利