{{ $t("message.ADVERTISEMENT") }}
{{ $t("message.AD_EXPIRE_DATE") }}2024年03月
文献
J-GLOBAL ID:201902235390234934   整理番号:19A2085358

ビジュアルプログラミングを用いたNuSMVのモデル生成支援環境

Visual Programming Language for Model-checker NuSMV
著者 (5件):
資料名:
巻: 119  号: 113(KBSE2019 11-22)(Web)  ページ: 41-46 (WEB ONLY)  発行年: 2019年07月05日 
JST資料番号: S0532B  ISSN: 0913-5685  資料種別: 会議録 (C)
記事区分: 原著論文  発行国: 日本 (JPN)  言語: 日本語 (JA)
抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
モデル検査は形式手法の一つで,網羅的かつ自動化された証明を可能とする非常に強力な技術である.しかしながら技術的な障壁の高さからモデル検査の利活用は十分に進んでいるとは言えない.本研究では,モデル検査の利用促進を目的として,モデル検査ツールの一つであるNuSMVのモデル生成を支援するビジュアルプログラミング環境を提案する.ビジュアルプログラミング言語にはブロック型やノード型と様々な形があるが,NuSMVではデータフローを表現したいので,ノード型のビジュアルプログラミング言語を提案する.提案するビジュアルプログラミング言語では変数ノード,状態ノード,条件判定ノード,初期値ノード,関数ノードの6つのノードから構成される.これらのノードを矢印でつなぎ合わせることで変数の値の変化を表現し,モデルの遷移関係を定義する.システムの持つ各変数に対してビジュアルプログラミングを行い,それを組み合わせ一つのSMVプログラムを生成する.このようなビジュアルプログラミングについて検討した.今後の課題としてプログラミング環境の実装が挙げられる.(著者抄録)
シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。

準シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。

分類 (1件):
分類
JSTが定めた文献の分類名称とコードです
計算機システム開発 
タイトルに関連する用語 (3件):
タイトルに関連する用語
J-GLOBALで独自に切り出した文献タイトルの用語をもとにしたキーワードです

前のページに戻る