文献

J-GLOBAL ID：201702221286718010   整理番号：17A1256722

動的プログラム実行としての完全正則時相特性検証【Powered by NICT】

Full Regular Temporal Property Verification as Dynamic Program Execution

著者 (3件)： Wang Meng ,  Tian Cong ,  Duan Zhenhua
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： ICSE-C  ページ： 226-228  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： コストはソースコードからモデルを抽出する高いためコードレベルでのプログラムの検証は益々注目を集めている。コードレベル検証のための利用可能なアプローチの大部分は,アサーションを挿入するプログラムに,アサーションは破られるかどうかをチェックすることにより行った。しかしこのようにして,安全性特性を検証することができ,活性のようなプログラムの他の時間的特性を検証することができない。この問題を解決するために,検証するプログラムをモデル化,シミュレーションおよび検証言語(MSVL)プログラムMで書かれているが本論文で提示した統一モデル検査アプローチと望ましい特性は,伝統的なモデル検査アプローチからのP.異なる命題投影時相論理(PPTL(命題投影時間論理))の式で記述し,所望の特性の否定はMSVLプログラムMの第一に変換した。PはMに有効であるかどうかは,新しいMSVLプログラムの許容実行「MおよびM’」が存在するかどうかを評価することにより確認することができた。この問題はMSVLのコンパイラすなわちMSVを実施できる。提案されたアプローチは,UMC4MSVLと呼ばれるツールに実装した。実験はUMC4MSVLは実世界プログラムの時間的特性を検証するのに有効であることを示した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： 命題 ,  モデル ,  言語 ,  *プログラム実行 ,  時間論理 ,  統一模型 ,  *位相特性 ,  安全性 ,  モデル検査 ,  コンパイラ ,  モデリング ,  忍容性
準シソーラス用語： 許容性 ,  アサーション ,  ソースコード , 【Automatic Indexing@JST】

分類 (2件)： 計算機システム開発  (JD02010R) ,  言語プロセッサ  (JD03040F)

タイトルに関連する用語 (3件)： プログラム実行 ,  相特性 ,  検証