ビジュアルプログラミングに基づくnuXmvのモデル作成支援ツールの開発

• Item type: SIG Technical Reports(1)
• 公開日: 2026-03-02
• タイトル / 言語: ja
• タイトル: ビジュアルプログラミングに基づくnuXmvのモデル作成支援ツールの開発
• タイトル / 言語: en
• タイトル: Development of an Environment for Supporting nuXmv Model Description based on Visual Programming
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 岡山県立大学
• 著者所属: 岡山県立大学
• 著者所属: 南山大学
• 著者所属: 愛媛大学
• 著者所属: 岡山県立大学
• 著者所属(英): en
• 著者所属(英): Okayama Prefectural University
• 著者所属(英): en
• 著者所属(英): Okayama Prefectural University
• 著者所属(英): en
• 著者所属(英): Nanzan University
• 著者所属(英): en
• 著者所属(英): Ehime University
• 著者所属(英): en
• 著者所属(英): Okayama Prefectural University
• 著者名: 濱,寿将; 横川,智教; 天嵜,聡介; 阿萬,裕久; 有本,和民
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: モデル検査は，システムを状態遷移系としてモデル化し，時相論理で記述した性質を満たすかどうかを自動判定できる．一方で，ツール固有言語でモデルを記述する必要があり，導入障壁が高い．先行研究では，Node-REDのノードグラフ型ビジュアルプログラミングを用いてNuSMV/nuXmv向けのモデル作成を支援するツールを開発し，作成コストの軽減を狙った．しかし，初学者を想定した評価ではツールの機能不足が明らかになり，Node-REDの制約が改善の障害となることが明らかとなった．そこで本研究では，これらの制約を回避し，初学者でも扱いやすいモデル検査支援環境を実現するため，React Flowを用いてnuXmvの検査用モデル作成インタフェースを実装する．さらに，先行研究で用いられていたノード群を再実装するとともに，Node-REDでは実装が難しかったノードや機能も追加する．また，ユーザビリティテストを通して，開発した環境の実用性と優位性を評価する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Model checking enables the automatic verification of whether a system, modeled as a state transition system, satisfies properties described in temporal logic. However, it requires modeling in tool-specific languages, which poses a high barrier to entry. Previous research aimed to reduce creation costs by developing a tool that supports model creation for NuSMV/nuXmv using Node-RED's node-graph-based visual programming. However, evaluations targeting beginners revealed functional deficiencies in the tool, and it became clear that the constraints of Node-RED hindered further improvements. Therefore, in this research, to bypass these constraints and realize a model checking support environment that is easy for beginners to handle, we implement an interface for creating nuXmv inspection models using React Flow. Furthermore, we reimplement the node groups used in the previous research and add nodes and functions that were difficult to implement in Node-RED. Additionally, we evaluate the practicality and superiority of the developed environment through usability testing.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2026-SE-222, 号 22, p. 1-8, 発行日 2026-03-02
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8825
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会