计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
11期
181-186,221
,共7页
通信顺序进程(CSP)%并发系统%迹模型%回答集编程(ASP)
通信順序進程(CSP)%併髮繫統%跡模型%迴答集編程(ASP)
통신순서진정(CSP)%병발계통%적모형%회답집편정(ASP)
Communicating sequential processes%Concurrent system%Trace model%Answer set programming
CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法.当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂；性质采用迹进行规范,不利于活性的描述.提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述.利用ASP(Answer Set Programming)技术实现了一个CSP验证系统.实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例.
CSP(Communicating Sequential Processes)是構建併髮繫統和網絡安全協議的經典方法.噹前主流的CSP模型驗證方法需將進程轉化為遷移繫統,轉化過程比較複雜；性質採用跡進行規範,不利于活性的描述.提齣瞭一種基于進程跡的CSP模型驗證框架,其性質採用通用的規範方法LTL進行描述.利用ASP(Answer Set Programming)技術實現瞭一箇CSP驗證繫統.實驗錶明,與類似繫統相比,該繫統的描述能力更彊,驗證結果的準確性更高,在性質不滿足時還可提供反例.
CSP(Communicating Sequential Processes)시구건병발계통화망락안전협의적경전방법.당전주류적CSP모형험증방법수장진정전화위천이계통,전화과정비교복잡；성질채용적진행규범,불리우활성적묘술.제출료일충기우진정적적CSP모형험증광가,기성질채용통용적규범방법LTL진행묘술.이용ASP(Answer Set Programming)기술실현료일개CSP험증계통.실험표명,여유사계통상비,해계통적묘술능력경강,험증결과적준학성경고,재성질불만족시환가제공반례.
