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

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

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

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