文献

J-GLOBAL ID：201902222735063032   整理番号：19A0049530

VASR-CBMC:バリオグラムに基づくマルチスレッドプログラム検証【JST・京大機械翻訳】

VSAR-CBMC :variable subgraph based multi-threaded program verification

著者 (3件)： Li Yunchou (北京跟踪与通信技術研究所,北京,100094) ,  Yin Ping (北京跟踪与通信技術研究所,北京,100094) ,  Yin Liangze (国防科技大学計算机学院,長沙,410073)
資料名： Jisuanji Yingyong Yanjiu  (Jisuanji Yingyong Yanjiu)
巻： 35  号： 8  ページ： 2393-2396  発行年： 2018年 
JST資料番号： C2536A  ISSN： 1001-3695  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： Yogar-CBMCはイベントシーケンス図に基づく反例抽象精密化思想を実現し、現在最も有効なマルチスレッドプログラム検証ツールの一つである。イベントシーケンス図が複雑であるため、反例の実行可能性を判断し、精緻化の制限時間が長いという問題を判断し、可変量子図の概念と可変量子図に基づく抽象精密化方法を提出し、グローバルイベントシーケンス図を連結等価の変量子図集に分解し、変量子図に基づいて反例検証と精緻化解決を行った。その結果,グラフの規模を効果的に縮小し,検証効率を改善した。提案方法をVSAR-CBMCに実装し,実験結果は,Yogar-CBMCと比較して,検証時間が平均43%短縮され,モデル検査が並列プログラムの検証能力を有効に改善できることを証明した。Data from Wanfang. Translated by JST.【JST・京大機械翻訳】

シソーラス用語： モデル検査 ,  精密化 ,  *プログラム検証 ,  *マルチスレッド
準シソーラス用語： 並列プログラム ,  反例 ,  シーケンス図 , 【Automatic Indexing@JST】

分類 (1件)： 計算機網  (JC03000K)

タイトルに関連する用語 (3件)： バリオグラム ,  マルチスレッド ,  プログラム検証