计算机科学
計算機科學
계산궤과학
Computer Science
2015年
10期
244-250,291
,共8页
通信顺序进程(CSP)%并发系统%Petri网%性质验证%安全性
通信順序進程(CSP)%併髮繫統%Petri網%性質驗證%安全性
통신순서진정(CSP)%병발계통%Petri망%성질험증%안전성
Communicating sequential processes (CSP)%Concurrent systems%Petri net%Property verification%Safety
通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具.CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足.Petri网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析.结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证.实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围.
通信順序進程(CSP)和Petri網是兩種重要的併髮繫統建模工具.CSP語言具有高度抽象性,可有效刻畫併髮進程之間的各種相互作用,但在物理結構的描述與驗證分析方麵顯得不足.Petri網是一種形式化、圖形化的併髮繫統建模和分析工具,側重于繫統的物理結構描述和性質分析.結閤兩者優點,首先利用CSP描述待驗證的併髮繫統,然後將其轉化為Petri網來分析繫統的動態行為特性,最後利用性質分析工具TINA對繫統性質進行分析和驗證.實驗結果錶明,傳統的CSP進程性質驗證工具不能驗證CSP進程的安全性,但其轉化為Petri網後可有效地分析齣導緻安全性不能滿足的危險因素,從而擴大瞭CSP描述的併髮繫統可驗證性質的範圍.
통신순서진정(CSP)화Petri망시량충중요적병발계통건모공구.CSP어언구유고도추상성,가유효각화병발진정지간적각충상호작용,단재물리결구적묘술여험증분석방면현득불족.Petri망시일충형식화、도형화적병발계통건모화분석공구,측중우계통적물리결구묘술화성질분석.결합량자우점,수선이용CSP묘술대험증적병발계통,연후장기전화위Petri망래분석계통적동태행위특성,최후이용성질분석공구TINA대계통성질진행분석화험증.실험결과표명,전통적CSP진정성질험증공구불능험증CSP진정적안전성,단기전화위Petri망후가유효지분석출도치안전성불능만족적위험인소,종이확대료CSP묘술적병발계통가험증성질적범위.
