擴展π演算的建模、驗證與測試.pdf

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

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

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

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

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

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