擴(kuò)展π演算的建模、驗(yàn)證與測試.pdf

1、時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)是以并發(fā)性、移動(dòng)性、時(shí)間相關(guān)性和異構(gòu)性等為主要特征的計(jì)算系統(tǒng)。對于這類系統(tǒng)，特別是安全攸關(guān)的時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)，如移動(dòng)支付系統(tǒng)、移動(dòng)通信系統(tǒng)、交通控制系統(tǒng)等，其失誤和崩潰可能會造成重大損失，因此時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)的正確性、安全性等質(zhì)量屬性受到人們的普遍重視。對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)采用以嚴(yán)格數(shù)學(xué)理論為支撐的形式化方法進(jìn)行建模、驗(yàn)證與測試是行之有效的減少系統(tǒng)設(shè)計(jì)錯(cuò)誤和保證系統(tǒng)質(zhì)量的重要途徑。
　　進(jìn)程代數(shù)，作為

2、形式化方法的代表，是一種重要的用于對并發(fā)系統(tǒng)進(jìn)行建模和驗(yàn)證的技術(shù)。由于所面向的領(lǐng)域和應(yīng)用背景的不同，涌現(xiàn)出很多進(jìn)程代數(shù)的分支和變種，其中π演算就是用于建模移動(dòng)性的重要的分支。近年來，由于新型網(wǎng)絡(luò)技術(shù)和信息技術(shù)的不斷發(fā)展，使得能夠建模和驗(yàn)證移動(dòng)系統(tǒng)的π演算得到人們的廣泛關(guān)注。但是，π演算在對系統(tǒng)建模時(shí)并未考慮到動(dòng)作執(zhí)行所占用的時(shí)間以及系統(tǒng)在某個(gè)狀態(tài)所持續(xù)的時(shí)間，故而，使得它不適于對時(shí)間相關(guān)系統(tǒng)進(jìn)行建模、驗(yàn)證和測試。
　　為了對時(shí)間相

3、關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和驗(yàn)證，本文研究了添加時(shí)間相關(guān)特性的擴(kuò)展的π演算。在此基礎(chǔ)上，提出采用擴(kuò)展π演算為時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和推演的方法。進(jìn)一步地，為了對擴(kuò)展π演算建模的系統(tǒng)進(jìn)行自動(dòng)驗(yàn)證，提出將擴(kuò)展π演算轉(zhuǎn)換為建模、仿真驗(yàn)證語言MSVL的方法。此外，為了對擴(kuò)展π演算建模的系統(tǒng)進(jìn)行測試，文章還給出了采用擴(kuò)展π演算的測試用例生成方法。所取得的研究成果主要有以下幾個(gè)方面。
　　(1)建立了帶區(qū)間動(dòng)作前綴的擴(kuò)展π演算p-π，定義了

4、p-π的語法和操作語義，給出了p-π的代數(shù)性質(zhì)和時(shí)間相關(guān)性質(zhì)并對其進(jìn)行了證明。在此基礎(chǔ)上給出了p-π對時(shí)間相關(guān)行為的建模。此外，還通過實(shí)例對p-π的應(yīng)用效果和相應(yīng)性質(zhì)所起的作用進(jìn)行了分析和說明。
　　(2)提出了采用擴(kuò)展π演算對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和推演的方法。采用區(qū)間動(dòng)作前綴和瞬時(shí)動(dòng)作前綴分別描述系統(tǒng)的時(shí)間相關(guān)行為和交互行為，并通過操作算子將子進(jìn)程進(jìn)行復(fù)合，然后利用操作規(guī)則構(gòu)造出系統(tǒng)的時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)和可接受的執(zhí)行路

5、徑，基于上述遷移系統(tǒng)和執(zhí)行路徑完成對系統(tǒng)性質(zhì)的推演。通過移動(dòng)車輛控制系統(tǒng)的分析表明，所提方法可對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行有效建模和推演，保證時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)的可靠性。
　　(3)提出了從擴(kuò)展π演算p-π到MSVL的轉(zhuǎn)換方法。為了完成轉(zhuǎn)換，先在MSVL中對通道和通信原語進(jìn)行了定義?；谠摱x，給出了從p-π到MSVL的結(jié)構(gòu)化轉(zhuǎn)換規(guī)則，并對二者采用的通信機(jī)制間存在的一致性進(jìn)行了證明。為了說明轉(zhuǎn)換的合理性，文章還證明在p-π進(jìn)程和M

6、SVL的格局間存在互模擬關(guān)系。這樣，通過轉(zhuǎn)換，就可以借助MSVL建模仿真驗(yàn)證工具完成對p-π進(jìn)程的驗(yàn)證。
　　(4)提出了基于擴(kuò)展π演算的測試用例生成方法。采用p-π為時(shí)間相關(guān)并發(fā)系統(tǒng)建模并由p-π的操作規(guī)則構(gòu)造出系統(tǒng)模型的時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)。基于時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)和用例規(guī)約生成測試用例，測試用例的生成滿足執(zhí)行動(dòng)作覆蓋準(zhǔn)則、路徑覆蓋準(zhǔn)則和時(shí)間約束覆蓋準(zhǔn)則，并給出了測試用例的選擇策略。同時(shí)通過p-π的驗(yàn)證方法，還保證了所產(chǎn)生的測