實時狀態(tài)圖的形式化及其應用研究.pdf

1、隨著智能化時代的到來,計算機軟件得到了廣泛應用。然而在實際應用中,小到隨身手機系統(tǒng)的頻頻崩潰,大到事關國計民生的鐵路信號、飛行控制等系統(tǒng)的不時故障,問題頻出。軟件系統(tǒng)質量的保障一直以來都是國內外研究的重點及熱點。需求說明是軟件系統(tǒng)開發(fā)的基礎和根本,因此對軟件需求的全面準確把握極其重要。目前,統(tǒng)一建模語言UML已廣泛應用于工業(yè)軟件需求的建模分析,但是,在面對軟件的非功能性需求以及時間苛求的軟件系統(tǒng)時,UML因其自身缺陷難以應對。同時,UM

2、L是半形式化的,其模型設計的正確性無法得到驗證,這必將為軟件系統(tǒng)后續(xù)的開發(fā)埋下隱患。時間Petri網作為一種兼具嚴格的數學表示及便捷友好的圖形化表達方式的形式化方法,已被成功應用于時間苛求系統(tǒng)的質量保障。因此,考慮到軟件非功能性需求中的時間因素,為了更好的保證時間苛求系統(tǒng)的質量,本文提出了“基于時間Petri網的UML狀態(tài)圖的形式化方法”,根據此方法初步實現了時間擴展狀態(tài)圖模型到時間Petri網模型的自動轉換工具timConvert。本

3、論文的主要研究工作如下:
　　1.針對狀態(tài)圖建模分析應用的現狀,為了更好的服務時間苛求系統(tǒng),本文給出了基于時態(tài)區(qū)間的標準狀態(tài)圖的時間擴展方法:
　　2.在對時間擴展后的狀態(tài)圖進行分析之后,提出了時間擴展狀態(tài)圖的形式化定義,并完成了對時間擴展狀態(tài)圖主要建模元素,相關基本性質的形式化描述:
　　3.為驗證時間擴展狀態(tài)圖建模結果,在分析和比對了時間擴展狀態(tài)圖和時間Petri網的語義及建模元素之后,提出了兩者之間的映射規(guī)則;<