隨著資訊科技的飛速發展，軟體規模和複雜性不斷增大，對軟體開發速度和質量的要求不斷提高。從而迫切需要一套簡單易行的方法來指導規模龐大、結構複雜的軟體開發過程。模型可以簡明、準確的表示複雜、抽象的系統，並且可以幫助設計者從全域性上把握系統的全貌及其相關部件之間的聯絡，防止設計者過早地陷入各個模組的細節之中。因此，在物件導向的軟體開發中，建模就顯得尤為重要，建模語言也一直是物件導向技術的研究重點。
本文共有七章，具體章節如下:
第一章為緒論部分。首先，討論了形式化方法的必要性和重要性，常用形式化驗證方法的基本原理、適用範圍，以及多種時序邏輯的語法和特點。然後，介紹了基於模型的測試方法，並對基於uml模型進行測試、驗證的相關工作進行了分析與比較。最後，詳細說明了本文的研究重點和主要工作。
第二章研究uml2.0序列圖的形式化描述方法。首先，簡要介紹了uml2.0序列圖的新特徵。然後，給出了序列圖的語法、語義，以及序列圖中單個物件的形式化定義。最後，定義了一種事件確定有限自動機作為序列圖的形式化模型，並給出了該自動機的構造演算法。
第三章研究基於uml2.0序列圖的形式化驗證方法。在討論命題投影時序邏輯的語法和語義基礎上，詳細說明了對軟體性質的描述方法以及基於事件確實有限自動機的pptl性質模型檢測演算法。
第四章在對序列圖形式化描述基礎上，提出了基於自動機的測試用例生成方法。首先，給出了復合自動機的定義，並介紹了4種合成規則，以此為基礎實現了自動機合成演算法。然後，通過定義的覆蓋準則、測試場景產生規則，以及測試用例生成演算法產生相應的測試用例集。
第五章研究分布式軟體系統互動行為的建模、驗證與測試方法。首先，通過定義的系統狀態機圖和物件狀態機圖分別對分布式系統中各獨立子系統的狀態轉換進行建模，並使用序列圖建模各子系統的互動行為。然後，採用模型檢測方法完成對互動行為的驗證。最後，討論了分布式軟體的測試框架和基於模型的測試用例產生。
第六章詳細介紹了序列圖的建模工具。說明了基於eclipse外掛程式的序列圖建模環境的設計，以及序列圖向事件確實有限自動機模型進行轉換的實現。
第七章是全文的總結與展望。總結了本文的工作，並對進一步的研究方向作出展望
[1]張琛. 基於uml2.0模型的測試與驗證方法[d].西安電子科技大學,2012.
畢業設計 文獻參考（十六）
如果把教學改革看作乙個系統工程，那麼教材管理就是這個系統工程的子工程，這個子工程一旦出現問題，那麼整個教學工作必將無法正常進行。教材徵訂與發放工作是教材管理的重要工作，如果教材徵訂與發放出現問題，同樣會使整個教學工作處於混亂與被動局面。為應對辦學形式多樣化和學生規模不斷擴大給教學管理帶來的壓力和度，...
畢業設計 文獻參考（十二）
電信業在近幾年得到了蓬勃的發展，業務更加複雜，關係更加緊密，資料更加多樣化。原先舊的綜合服務保障系統逐漸顯露出自身架構的缺陷 所有功能集中在乙個專案中，邏輯複雜 模組耦合 臃腫，修改難度大，系統錯誤隔離性差 可用性差，任何乙個模組的錯誤均可能造成整個系統的宕機。eureka ribbon hystr...
畢業設計 文獻參考（14）
隨著無線通訊技術可靠性及可用性的提高，基於通訊的列車控制方式已成為國際上高速列車控制系統的主要發展方向。我國的 級列車執行控制系統正是一種基於通訊的列車執行控制系統，通過無線通訊實現車地間連續 雙向的資訊傳輸，利用無線閉塞中心 產生的行車許可以及其他與列車執行控制有關的資訊來保障列車的安全高速執行 ...