基于場(chǎng)景和屬性的需求引出及形式化建模.pdf

1、場(chǎng)景是一種分析與驗(yàn)證需求的有效工具,因此基于場(chǎng)景的分析與設(shè)計(jì)受到廣泛關(guān)注。場(chǎng)景提供預(yù)期系統(tǒng)的行為實(shí)例,也就是說場(chǎng)景中的交互行為一定是預(yù)期系統(tǒng)要出現(xiàn)的行為。一個(gè)場(chǎng)景一般情況下不能完整的描述整個(gè)系統(tǒng)的行為,所以基于單個(gè)場(chǎng)景構(gòu)建的行為模型只是最終預(yù)期系統(tǒng)的一個(gè)下界。屬性是描述系統(tǒng)行為必須要滿足的一種狀態(tài)說明,基于屬性的構(gòu)造的行為模型包含所有不違反屬性的可能軌跡。因此基于屬性的行為建模為預(yù)期系統(tǒng)提供了一個(gè)上界。如何基于場(chǎng)景構(gòu)造預(yù)期系統(tǒng)的下界和基

2、于屬性構(gòu)造預(yù)期系統(tǒng)的上界,以及在上界行為模型和下界行為模型之間得到最終的預(yù)期系統(tǒng)便是本文的研究重點(diǎn)。
　　 本文首要解決是如何進(jìn)行基于場(chǎng)景和屬性的需求引出。消息序列圖(MessageSequence Charts,MSC),一種場(chǎng)景的表示方法,用于描述場(chǎng)景中構(gòu)件之間的通信、交互行為,因此本文首先介紹MSC的基本概念。3-值流體線性時(shí)序邏輯公式是一種描述系統(tǒng)屬性的有效方法,因此在介紹3-值克萊尼邏輯(Kleene logic)和流

3、體之后,文中給出了3-值流體線性時(shí)序邏輯公式的概念。然后通過一個(gè)論壇發(fā)帖系統(tǒng)的實(shí)例,根據(jù)場(chǎng)景的描述將需求引出,生成MSC圖,然后又將需求形式化為屬性描述。
　　 基于場(chǎng)景合成的標(biāo)號(hào)遷移系統(tǒng)只能描述場(chǎng)景給出的行為,不能描述場(chǎng)景沒有給出的可能行為。基于屬性合成的標(biāo)號(hào)遷移系統(tǒng)不能區(qū)分哪些是為了滿足安全屬性必須發(fā)生的行為和不違反安全屬性的可能發(fā)生的行為。針對(duì)現(xiàn)有合成算法存在的問題,并在現(xiàn)有合成算法的基礎(chǔ)上,我們給出了合成模態(tài)遷移系統(tǒng)的算

4、法。在現(xiàn)有基于場(chǎng)景合成LTS算法的基礎(chǔ)上,提出一個(gè)算法使得LTS變成MTS,得到一個(gè)預(yù)期系統(tǒng)必然行為的下界,同時(shí)合成的MTS模型可以表達(dá)除場(chǎng)景描述之外的可能行為。在基于屬性合成LTS算法的基礎(chǔ)上,提出了合成MTS的算法,得到預(yù)期系統(tǒng)的一個(gè)上界,合成的MTS模型可以區(qū)分必然行為和可能行為。最后通過合并操作將這兩個(gè)MTS模型合并為一個(gè)MTS,該模型保留下界的必然行為和上界的可能行為。合并之后,系統(tǒng)行為可以進(jìn)一步精化,模態(tài)遷移系統(tǒng)的精化不僅保