文献

J-GLOBAL ID：201702223756976064   整理番号：17A1774648

一次BDDによる時間論理モニタリング【Powered by NICT】

First order temporal logic monitoring with BDDs

著者 (3件)： Havelund Klaus (Jet Propulsion Laboratory, California Inst. of Technology, USA) ,  Peled Doron (Department of Computer Science Bar Ilan University, Israel) ,  Ulus Dogan (Verimag/Universite ́ Grenoble-Alpes, Grenoble, France)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FMCAD  ページ： 116-123  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 実行時検証は,実行中のプログラムやシステムに由来する実行トレースを分析することを目的としている。伝統的な目的は,形式的仕様記述に関する適合性の欠如を検出することである。分野における多くの努力は,いわゆるパラメトリック仕様をモニタリングに焦点を当てた,イベントは,データを,公式は,このようなを参照できる。このような仕様のためのモニターは観察されたデータを保存しなければならないので,挑戦は,論理演算子,定量およびルックアップデータの効率的な表現と操作を持つことである。基本的な問題は,データの実際の値が有界または提供される事前に必ずしもないことである。本研究では,観測データを表現するための二分決定グラフ(BDD)の使用を検討した。著者らの実験は,関連研究に比べて性能のかなりの改善を示した。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件)： システムモデル  (IB02000Z) ,  信頼性  (KB04040H)

タイトルに関連する用語 (3件)： BDD ,  時間論理 ,  モニタリング