實時系統(tǒng)的運行時驗證研究.pdf

1、在國民經(jīng)濟與國防現(xiàn)代化建設中，計算機軟件在日常生活中的應用越來越普及，軟件可靠性問題日趨受到人們的重視，尤其對于一些安全關(guān)鍵領(lǐng)域，如載人航天、高速軌道交通等。應用于這些領(lǐng)域的系統(tǒng)通常是實時控制系統(tǒng)，這類系統(tǒng)不僅要求系統(tǒng)做出正確的響應，且要求系統(tǒng)的響應滿足相應的時間約束。系統(tǒng)一旦發(fā)生失效，將會給國家安全乃至人員生命帶來極大損失，因此如何提高這類系統(tǒng)的可靠性成為目前計算機領(lǐng)域的一個非常重要的研究內(nèi)容。傳統(tǒng)的測試方法由于存在測試用例不完備等問

2、題無法滿足系統(tǒng)的可靠性需求，模型檢測能給出系統(tǒng)完備的正確性證明，但是對于復雜系統(tǒng)來說，這一技術(shù)面臨著狀態(tài)空間爆炸等問題。運行時驗證作為測試和模型檢測的有效補充，在系統(tǒng)運行過程中實施有效地監(jiān)控與驗證，盡早地發(fā)現(xiàn)軟件失效，有助于提高實時系統(tǒng)的安全性和可靠性。
　　為了提高實時系統(tǒng)的安全性和可靠性，本文提出一種基于度量區(qū)間時序邏輯(Metric Interval Temporal Logic，MITL)三值語義的運行時驗證方法，主要工作

3、如下:
　　1、介紹了pointwise語義模型下MITL在有窮軌跡上的語法及語義，采用pointwise語義模型是因為MITL在該語義模型下是可判定的，定義了MITL在有窮軌跡上的三值語義，與LTL三值語義不同的是，它是在有窮時間字上進行解釋的。
　　2、本文定義了基于MITL三值語義的監(jiān)控器的形式化描述，即基于遷移的擴展時間Buchi自動機(transition-based generalized timed Buchi

4、 automaton，TGTBA)，它是在基于遷移的擴展Buchi自動機的基礎(chǔ)上，通過增加時鐘約束得到的。在此基礎(chǔ)上，研究了一種構(gòu)造預測監(jiān)控器的方法，即采用邏輯重寫的方法，根據(jù)給出的重寫算法將公式重寫為要求的形式，基于重寫后的公式來構(gòu)造TGTBA，將此TGTBA作為MITL公式的預測監(jiān)控器，用于運行時驗證過程中。
　　3、在上述驗證方法和MaC驗證框架的基礎(chǔ)上，將基于MITL的預測監(jiān)控器應用于MaC框架中，實現(xiàn)了基于MITL三值語