基于Petri網(wǎng)的CSP并發(fā)系統(tǒng)驗(yàn)證技術(shù)研究.pdf

1、通信順序進(jìn)程 CSP是一種高度抽象的形式化描述語言，具有嚴(yán)格的數(shù)學(xué)理論支撐，可有效刻畫并發(fā)系統(tǒng)進(jìn)程之間的各種相互作用。然而，在 CSP并發(fā)系統(tǒng)的驗(yàn)證方面，由于其本身特性所限，還存在以下不足：1)用CSP語言描述的并發(fā)系統(tǒng)沒有反映系統(tǒng)的物理結(jié)構(gòu)信息，不便于與此相關(guān)的系統(tǒng)特性的分析和驗(yàn)證；2)盡管對并發(fā)有一定的刻畫，但不能全面反映復(fù)雜系統(tǒng)的真實(shí)并發(fā)行為。Petri網(wǎng)是一種形式化、圖形化的并發(fā)系統(tǒng)建模和分析工具，雖然在原始模型抽象方面不如CS

2、P，但能夠精確地分析系統(tǒng)的靜態(tài)特性和動態(tài)行為性質(zhì)，側(cè)重于系統(tǒng)的物理結(jié)構(gòu)描述和性質(zhì)分析。
　　本文將Petri網(wǎng)技術(shù)引入CSP并發(fā)系統(tǒng)驗(yàn)證將有助于彌補(bǔ)單純基于CSP分析來驗(yàn)證系統(tǒng)性質(zhì)的不足。首先利用CSP描述待驗(yàn)證的并發(fā)系統(tǒng)，將其關(guān)鍵跡轉(zhuǎn)化為Petri網(wǎng)來分析系統(tǒng)的行為特性；然后利用性質(zhì)分析工具 TINA對系統(tǒng)性質(zhì)進(jìn)行分析和驗(yàn)證。實(shí)驗(yàn)結(jié)果表明，CSP并發(fā)系統(tǒng)轉(zhuǎn)化為Petri網(wǎng)后可有效地分析出導(dǎo)致安全性不能滿足的危險因素，從而擴(kuò)大了

3、CSP描述的并發(fā)系統(tǒng)可驗(yàn)證性質(zhì)的范圍。本文主要研究內(nèi)容如下：
　?。?）討論CSP進(jìn)程到Petri網(wǎng)的轉(zhuǎn)換規(guī)則。該部分包括CSP關(guān)鍵跡模型的基本進(jìn)程到Petri網(wǎng)的轉(zhuǎn)換規(guī)則以及CSP并發(fā)操作到Petri網(wǎng)的轉(zhuǎn)換規(guī)則，基本進(jìn)程包括前綴、遞歸、確定性選擇和非確定性選擇。并發(fā)操作包括交互、并發(fā)和穿插，同時，給出基于Petri網(wǎng)的條件約束，保證轉(zhuǎn)換后Petri網(wǎng)的完整性。
　?。?）研究 CSP進(jìn)程與轉(zhuǎn)換后 Petri網(wǎng)的等價關(guān)系。

4、基于關(guān)鍵跡模型驗(yàn)證的等價性，證明了 CSP龐大的跡模型與關(guān)鍵跡模型在描述和性質(zhì)驗(yàn)證方面是等價的，因此將關(guān)鍵跡轉(zhuǎn)換為 Petri網(wǎng)與普通跡轉(zhuǎn)換之間具有等價性，但是關(guān)鍵跡效率更高。在討論CSP進(jìn)程與轉(zhuǎn)換后Petri網(wǎng)的等價性時，通過運(yùn)用Petri網(wǎng)語言和CSP的順序組件等相關(guān)知識，給出了兩種模型在等價性方面的理論證明。
　?。?）實(shí)例分析，以鐵路公路交叉口交通控制器為例，運(yùn)用上述方法，對轉(zhuǎn)換后的Petri網(wǎng)進(jìn)行可達(dá)樹分析，利用工具TI