文献

J-GLOBAL ID：201702288475081770   整理番号：17A0204958

MSVLを有する同時実行システムのモデル検査【Powered by NICT】

Model checking concurrent systems with MSVL

著者 (3件)： Zhang Nan (Institute of Computing Theory and Technology, Xidian University) ,  Duan Zhenhua (Institute of Computing Theory and Technology, Xidian University) ,  Tian Cong (Institute of Computing Theory and Technology, Xidian University)
資料名： Science China. Information Sciences  (Science China. Information Sciences)
巻： 59  号： 11  ページ： 118101-1-118101-3  発行年： 2016年 
JST資料番号： C2579A  ISSN： 1674-733X  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 英語 (EN)

抄録/ポイント： ClarkeとEmerson[1]ならびにQueilleとSifakis[2]によって提案されたモデル検査はハードウエア及びソフトウエアシステムに対する自動検証手法である。しかし,Clarkeを指摘[3]として,モデル検査は,(1)状態爆発問題,典型的には議論システムの並列成分またはデータ要素の数の指数関数的成長モデルにより引き起こされるに苦しんでいる(2)種々の表記法はシステムと必要な特性をモデル化するために用いた;(3)線形時間論理(LTL)と計算木論理(CTL)のような最もしばしば用いられる時相論理の表現力が弱くなる。これらの問題を克服するために,計算機科学者は,元のモデル検査に顕著な進歩を遂げた。最も顕著な改善は,組成,半順序[4],記号[5],有界[6]と抽象モデル検査[7+8]であった。Data from the ScienceChina, LCAS. Translated by JST【Powered by NICT】

シソーラス用語： 時間論理 ,  ハードウェア ,  表記法 ,  モデリング ,  計算機科学 ,  指数関数 ,  *モデル検査 ,  半順序
準シソーラス用語： 有界 ,  表現力 ,  線形時間論理 ,  成長モデル ,  状態爆発問題 , 【Automatic Indexing@JST】

分類 (2件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (1件)： モデル検査