文献

J-GLOBAL ID：201802228635422955   整理番号：18A0609896

統計的モデル検査による確率SystemCモデルの形式的検証【Powered by NICT】

Formal verification of probabilistic SystemC models with statistical model checking

著者 (2件)： Ngo Van Chan (Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA) ,  Legay Axel (Inria Rennes - Bretagne Atlantique, Rennes, 35042, France)
資料名： Journal of Software: Evolution and Process  (Journal of Software: Evolution and Process)
巻： 30  号： 3  ページ： ROMBUNNO.1890  発行年： 2018年 
JST資料番号： W0214A  ISSN： 2047-7473  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： SystemCと取引レベルのモデル化は,高レベル実行可能モデル,それらの多くは固有の確率的挙動,例えば,ランダムデータおよび低信頼性特徴成分を提供することにより,組込みシステムの挙動の記述に非常に成功している。システム特性の確率の定量的および定性的解析をすることが重要である。このような解析は,検証システムの形式的モデルを構築し,確率的モデル検査を用いて行うことができる。しかし,この方法は大規模システムのための実行不可能,状態空間爆発に起因していた。本論文では,大きなSystemCモデルから直接そのような解析を行い,設計者は広い範囲の有用な特性と形状を表現するために考慮した統計的モデル検査の成功した使用を実証した。本研究の最初の貢献は,時間と確率的特性との両方を有するSystemCモデルのための有界線形時相論理で表現された特性を検証するためのフレームワークである。第二に,フレームワークは,有界線形時相論理における原子命題としてユーザコードプリミティブの豊富な集合を明らかにすることを可能にした。さらに,ユーザはユーザ自身の細粒時間分解能よりもむしろSystemCシミュレーションにおけるクロックサイクルの境界を定義することができる。第三の寄与は統計的モデルチェッカーの実装である。モデルの下での検証の実行トレース,モデルの下での検証を装備自動機構,および統計的モデル検査アルゴリズムとの相互作用を生成するための自動モニタ生成を含んでいる。Copyright 2018 Wiley Publishing Japan K.K. All Rights reserved. Translated from English into Japanese by JST.【Powered by NICT】

シソーラス用語： 監視装置 ,  信頼性 ,  *モデル検査 ,  大規模系 ,  シミュレーション ,  モデリング ,  確率モデル ,  相互作用 ,  アルゴリズム ,  組込みシステム ,  システム特性
準シソーラス用語： 線形時間論理 ,  有界 ,  状態空間 ,  *SystemC , 【Automatic Indexing@JST】

著者キーワード (5件)： 確率的時間的主張 ,  プログラム検証 ,  実行時検証 ,  統計的モデル検査 ,  SystemCモデル

分類 (2件)： 計算理論  (JB02000A) ,  応用プログラミング言語  (JD03052Y)

タイトルに関連する用語 (6件)： 統計 ,  モデル検査 ,  確率 ,  SystemC ,  モデル ,  形式的検証