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

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

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

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

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