@techreport{oai:ipsj.ixsq.nii.ac.jp:02007722,
 author = {濱,寿将 and 横川,智教 and 天嵜,聡介 and 阿萬,裕久 and 有本,和民},
 issue = {22},
 month = {Mar},
 note = {モデル検査は，システムを状態遷移系としてモデル化し，時相論理で記述した性質を満たすかどうかを自動判定できる．一方で，ツール固有言語でモデルを記述する必要があり，導入障壁が高い．先行研究では，Node-REDのノードグラフ型ビジュアルプログラミングを用いてNuSMV/nuXmv向けのモデル作成を支援するツールを開発し，作成コストの軽減を狙った．しかし，初学者を想定した評価ではツールの機能不足が明らかになり，Node-REDの制約が改善の障害となることが明らかとなった．そこで本研究では，これらの制約を回避し，初学者でも扱いやすいモデル検査支援環境を実現するため，React Flowを用いてnuXmvの検査用モデル作成インタフェースを実装する．さらに，先行研究で用いられていたノード群を再実装するとともに，Node-REDでは実装が難しかったノードや機能も追加する．また，ユーザビリティテストを通して，開発した環境の実用性と優位性を評価する．, 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.},
 title = {ビジュアルプログラミングに基づくnuXmvのモデル作成支援ツールの開発},
 year = {2026}
}