文献

J-GLOBAL ID：201702219605093423   整理番号：17A0355062

パラメータ化実行時の検証研究とツールの実現【JST・京大機械翻訳】

Research on Parametric Runtime Verification and Tool Implementation

著者 (4件)： Wang Zhemin (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics) ,  Chen Zhe (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics) ,  Zhu Yunlong (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics) ,  Huang Zhiqiu (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics)
資料名： Xiaoxing Weixing Jisuanji Xitong  (Xiaoxing Weixing Jisuanji Xitong)
巻： 37  号： 12  ページ： 2667-2672  発行年： 2016年 
JST資料番号： C2136A  ISSN： 1000-1220  CODEN： XWJXEH  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： ソフトウェア規模の増加に伴い、ソフトウェアの信頼性と安全性を如何に保証するかは学術界と産業界でますます注目される問題になっている。実行時の検証は新しいプログラム自動検証技術であり、静的分析とモデル検査などの常用方法の欠点を補っている。本論文は,Cプログラムのための形式的仕様を記述するために,Cプログラムのためのモニタ仕様言語を設計した。この言語は有限状態オートマトンと正規表現に基づくパラメータ化実行時に検証される。本論文では,オープンソースツールツールとBISONを用いて,この言語をサポートするパラメータ化実行時の検証ツールMOVEC.を実現した。実行時に発生する大量のモニタに対して索引を行うために、著者らは1種の階層ハッシュ森林のデータ構造を提案し、実現した。実験結果は,このツールが実行可能で効率的であることを示した。Data from the ScienceChina, LCAS. Translated by JST【JST・京大機械翻訳】

シソーラス用語： モデル検査 ,  言語 ,  ソフトウェア ,  形式的仕様 ,  有限状態機械 ,  信頼性 ,  監視装置 ,  正規表現 ,  安全性 ,  仕様記述言語 ,  *パラメタリゼーション ,  データ構造

著者キーワード (4件)： runtime verification ,  formal specification ,  hierarchical hash table forest ,  finite state machine

分類 (2件)： オートマトン理論  (JB04000O) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (4件)： パラメータ化 ,  検証 ,  研究 ,  ツール