【文章內(nèi)容簡介】 間。 ? 解決由多個系統(tǒng)模型的并行組合而形成的狀態(tài)空間爆炸問題。 解決狀態(tài)空間爆炸問題的途徑 ? 狀態(tài)空間的符號表示 （ Symbolic representation of state space） McMillan’ s ordered binary decision diagrams (OBDD), 1992, 10120 ? 偏序規(guī)約技術(shù)（ Partial order reduction） ? 抽象技術(shù)（ Abstraction） ? 對稱技術(shù)（ Symmetry） 模型檢驗 ? 關(guān)于具有時序性質(zhì)的并發(fā)系統(tǒng)的模型檢驗理論和技術(shù)在工業(yè)界已經(jīng)得到實際的應(yīng)用。 ? 目前模型檢驗理論和技術(shù)的研究熱點已經(jīng)轉(zhuǎn)向?qū)崟r系統(tǒng)和軟件系統(tǒng)。 實時和混成系統(tǒng)的模型檢驗 對于實時系統(tǒng)來說，由于時間的引入，其狀態(tài)空間是無窮的。要設(shè)法遍歷無窮的狀態(tài)空間，這對研究人員來說是一個新的挑戰(zhàn)。目前人們關(guān)注的主要問題包括： ? 針對典型實時性質(zhì)開發(fā)檢驗算法 ? 探索解決狀態(tài)空間過大的有效途徑 混成系統(tǒng) 混成系統(tǒng)（ Hybrid Systems）是一類復(fù)雜的計算機系統(tǒng)，這類系統(tǒng)的運行過程中既有連續(xù)的狀態(tài)變化，又有離散的狀態(tài)變化。 混成系統(tǒng)實例 水箱監(jiān)控系統(tǒng) 混成系統(tǒng)實例 水箱監(jiān)控系統(tǒng) ? 初始狀態(tài)時，水箱中水面的高度為 1英寸； ? 水泵打開時，水箱中水面以每秒 1英寸的速度上升； ? 水泵關(guān)閉時，水箱中水面以每秒 2英寸的速度下降； ? 監(jiān)控器發(fā)出信號打開（關(guān)閉）水泵到實際打開（關(guān)閉）水泵之間有 2秒鐘的延遲； 要求監(jiān)控器將水箱中的水面高度控制在 1至 12英寸之間。 混成自動機（ hybrid automata） S1 x = 1 y = 1 y ? 10 S2 x = 1 y = 1 x ? 1 S3 x = 1 y = 2 x ? 2 S4 x = 1 y = 2 y ? 5 y=1 . . . . . . . . y = 10? x := 0 y = 5? x := 0 x = 2? x = 2? 混成自動機（ hybrid automata） ? 混成自動機是不可判定的； ? 目前國際上相關(guān)領(lǐng)域的研究熱點在于尋找混成自動機的可判定子集。 線性時段性質(zhì) 線性時段性質(zhì)可以通過系統(tǒng)在各個狀態(tài)上的累積時間來約束系統(tǒng)的行為。一個線性時段性質(zhì)是如下形式的線性積分不等式： ∑i∈ e ci∫si≤M 其中 si表示系統(tǒng)狀態(tài) ， ci是實型系數(shù)， M是實數(shù)。 線性時段性質(zhì) 在水箱監(jiān)控系統(tǒng)中 ,要求監(jiān)控器將水箱中的水面高度控制在 1至 12寸之間，可以表示成以下線性時段性質(zhì)： ? ∫s1 + ∫s2 2(∫s3 + ∫s4 ) ? 11 ? ∫s1 + ∫s2 2(∫s3 + ∫s4 ) ? 0 滿足性問題 檢驗混成自動機相對于線性時段性質(zhì)的滿足性問題： ? 一個混成自動機滿足一個線性時段性質(zhì)當且僅當該混成自動機的所有行為滿足該線性時段性質(zhì)。 混成自動機的行為表示 混成自動機的行為可以表示如下時間狀態(tài)序列： (s1, t1)^ (s2, t2)^…^ (s m, tm) 其中 si表示系統(tǒng)狀態(tài)， ti表示系統(tǒng)在 si上的停留時間 , t1, t2,…, t m必須滿足相應(yīng)的時間約束。 帶時段約束的規(guī)則表達式 在規(guī)則表達式中引入時段約束形成帶時段約束的規(guī)則表達式。時段約束表示成如下形式： a ? ∑i∈ e ci∫si ? b 帶時段約束的規(guī)則表達式 R = ? ? s0 ? (s0 ^ (s1 ,{∫s1 = 9}) ^ R1) ? (s0 ^ (s1 ,{∫s1 = 9}) ^ R1 ^ (s2, {∫s2 = 2})) ? (s0 ^ (s1 ,{∫s1 = 9}) ^ R1 ^ (s2 ^ s3 , {∫s2 = 2, 2∫s3 ∫s2 = 5})) ? (s0 ^ (s1 ,{∫s1 = 9}) ^ R1 ^ (s2 ^ s3 ^ s4, {∫s2 = 2, 2∫s3 ∫s2 = 5, ∫s2 = 2})) 其中 R1 = (s2 ^ s3 ^ s4^ s1 , {∫s2 = 2, 2∫s3 ∫s2 = 5, ∫s2 = 2, ∫s1 2∫s4 = 5 })* 帶時段約束的規(guī)則表達式 ? 帶時段約束的規(guī)則表達式不能描述所有混成自動機的行為； ? 帶時段約束的規(guī)則表達式對應(yīng)于一類混成自動機； ? 對應(yīng)于帶時段約束的規(guī)則表達式的一類混成自動機是可判定的。 基于線性規(guī)劃的驗證途徑 ? 用帶時段約束的規(guī)則表達式描述混成自動機的行為，從而線性時段性質(zhì)相對于混成自動機的滿足性問題轉(zhuǎn)化成為相對于規(guī)則表達式的滿足性問題； 基于線性規(guī)劃的驗證途徑 ? 對于不包含 *運算符的簡單規(guī)則表達式，由于規(guī)則表達式中所包含的時段約束形成了多組線性不等式，同時線性時段性質(zhì)本身可以作為相應(yīng)的目標函數(shù)，因此驗證滿足性問題可以轉(zhuǎn)化為一組線性規(guī)劃問題； 基于線性規(guī)劃的驗證途徑 ? 對于任意包含 *運算符的一般規(guī)則表達式 R，我們可以找出一個簡單規(guī)則表達式 R’，使得 R和R’在相對于某個給定的線性時段性質(zhì) P的滿足性問題上是等價的，即 R 滿足 P 當且僅當 R’ 滿足 P 從而最終將驗證滿足性問題歸結(jié)為線性規(guī)劃問題。 模型檢驗工具 Software Reuse （軟件復(fù)用） ? 軟件復(fù)用定義 ? 軟件復(fù)用過程 ? 軟件復(fù)用種類和形式 ? 軟件復(fù)用經(jīng)濟學(xué) ? 構(gòu)件 ? 軟件體系結(jié)構(gòu) 軟件復(fù)用定義 ? 軟件復(fù)用是指通過對已有軟件的各種有關(guān)知識來建立新的軟件，這些知識包括：領(lǐng)域知識、開發(fā)經(jīng)驗、設(shè)計經(jīng)驗、設(shè)計決定、體系結(jié)構(gòu)、需求、設(shè)計、編碼、測試和文檔等。 ? 軟件復(fù)用的目的是降低軟件開發(fā)和維護的成本，提高軟件開發(fā)效率，提高軟件的質(zhì)量。 可復(fù)用的軟件制品 Caper Jones定義了可作為復(fù)用候選的 10種軟件制品（ artifacts)： ? 項目計劃：軟件項目計劃的基本結(jié)構(gòu)和許多內(nèi)容（如進度表、風(fēng)險分析）都可以跨項目復(fù)用，以減少用于制定計劃的時間。 ? 成本估計：由于不同的項目中經(jīng)常含有類似的功能，所以有可能在極少修改或不修改的情況下，復(fù)用對該功能的成本估計。 ? 體系結(jié)構(gòu)：某些應(yīng)用軟件的體系結(jié)構(gòu)往往非常相似，因此有可能創(chuàng)建一組公共的體系結(jié)構(gòu)模板（如，事物處理體系結(jié)構(gòu)），并將那些模板作為可復(fù)用的設(shè)計框架。 ? 需求模型和規(guī)約：類和對象模型及其