文献

J-GLOBAL ID：202002249065218005   整理番号：20A2692454

BDDによる一次時間論理モニタリング【JST・京大機械翻訳】

First-order temporal logic monitoring with BDDs

著者 (3件)： Havelund Klaus (Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, USA) ,  Peled Doron (Department of Computer Science, Bar Ilan University, Ramat Gan, Israel) ,  Ulus Dogan (Boston University, Boston, MA, USA)
資料名： Formal Methods in System Design  (Formal Methods in System Design)
巻： 56  号： 1-3  ページ： 1-21  発行年： 2020年 
JST資料番号： W4375A  ISSN： 0925-9856  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： ランタイム検証は,実行プログラムまたはシステムからの実行追跡の解析を狙った。従来の目的は,形式的仕様に関する適合の欠如を検出することである。現場における多くの努力は,事象がデータを運ぶパラメータ仕様の監視に焦点を当て,公式はそのようなように言及できる。そのような仕様のモニタは観測データを貯蔵しなければならないので,その課題は,Boole演算子,定量化,およびデータの検索の効率的な表現と操作を有することである。基本的な問題は,データの実数値が必ずしも有界で,前もって提供されることである。本研究では,観測データを表現するための二値決定ダイアグラムの使用を検討した。著者らの実験は,関連する研究と比較して,性能の大幅な改善を示した。Copyright Springer Science+Business Media, LLC, part of Springer Nature 2019 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 実数 ,  *時間論理 ,  形式的仕様
準シソーラス用語： 有界 , 【Automatic Indexing@JST】

著者キーワード (3件)： 過去の時間論理 ,  データ ,  BDD

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

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