| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2025-01-12 11:15 LLMを用いたPlantUML記述からNuSMVへの自動変換方法 ○井上歓聖・二ノ宮健来・小形真平・岡野浩三（信州大）  MSS2024-45 SS2024-24 |
|
| 抄録 | （和） | 状態遷移図の作成や，モデル検査式の記述には，高度な専門知識が要求される．このプロセスは基本的に手作業によって行われるが，多大な労力と正確性を確保するための技術が必要となる．そこで本研究では大規模言語モデル(LLM)の一つであるChatGPTを活用するアプローチを提案する．本研究では2つの新たな手法を提案する．PlantUMLで記述された状態遷移図を入力として使用し，形式検証ツールNuSMVで用いるモデル検査式を自動生成する手法を検討した．また生成したNuSMVコードを入力として検査項目を自動生成する手法について検討した．生成されたモデル検査コード及び検査項目を実際に検証し，それらが期待される結果を適切に導き出せるかを確認した．「話題沸騰ポット(第7版)」のタイマーボタンに関する状態遷移図に適用した．実験の結果，少しの手直しを加えることでNuSMVのモデル検査コードが実用的に使用可能であるという結果が得られた． |
| （英） | The creation of state transition diagrams and the description of model checking formulas require advanced expertise． This process is typically performed manually and demands considerable effort and technical skills to ensure accuracy．In response to these challenges，this study proposes an approach utilizing ChatGPT，one of the large language models (LLMs)．Specifically，we propose new two methods． The first method explores the automatic generation of model checking formulas for the formal verification tool NuSMV，using state transition diagrams described in PlantUML as input． The second method examines the automatic generation of verification items using the generated NuSMV code as input．The generated model checking code and verification items were validated to confirm whether they could appropriately derive the expected results．For the experiment，we used the state transition diagram related to the timer button of the product ``Hot Topic Pot (7th Edition)'' and conducted specific verifications．As a result of the experiment，minor adjustments enabled the NuSMV model checking code to be practically usable． | |
| キーワード | （和） | 形式手法 / NuSMV / LLM / プロンプトエンジニアリング / / / / |
| （英） | Formal Methods / NuSMV / LLM / Prompt Engineering / / / / | |
| 文献情報 | 信学技報, vol. 124, no. 326, SS2024-24, pp. 19-24, 2025年1月. | |
| 資料番号 | SS2024-24 | |
| 発行日 | 2025-01-05 (MSS, SS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2024-45 SS2024-24 |
|
| 研究会情報 | |
| 研究会 | MSS SS |
| 開催期間 | 2025-01-12 - 2025-01-13 |
| 開催地（和） | 鹿児島大学郡元キャンパス |
| 開催地（英） | |
| テーマ（和） | システム数理と応用，ソフトウェアサイエンスおよび一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2025-01-MSS-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | LLMを用いたPlantUML記述からNuSMVへの自動変換方法 |
| サブタイトル（和） | |
| タイトル（英） | Automatic Translation from PlantUML description to NuSMV using LLM |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 形式手法 / Formal Methods |
| キーワード(2)（和/英） | NuSMV / NuSMV |
| キーワード(3)（和/英） | LLM / LLM |
| キーワード(4)（和/英） | プロンプトエンジニアリング / Prompt Engineering |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 井上 歓聖 / Kansei Inoue / イノウエ カンセイ |
| 第1著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ) |
| 第2著者 氏名（和/英/ヨミ） | 二ノ宮 健来 / Takeki Ninomiya / ニノミヤ タケキ |
| 第2著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ) |
| 第3著者 氏名（和/英/ヨミ） | 小形 真平 / Shinpei Ogata / オガタ シンペイ |
| 第3著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ) |
| 第4著者 氏名（和/英/ヨミ） | 岡野 浩三 / Kozo Okano / オカノ コウゾウ |
| 第4著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ) |
| 講演者 | 第1著者 |
| 発表日時 | 2025-01-12 11:15:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | MSS2024-45, SS2024-24 |
| 巻番号（vol） | vol.124 |
| 号番号（no） | no.325(MSS), no.326(SS) |
| ページ範囲 | pp.19-24 |
| ページ数 | 6 |
| 発行日 | 2025-01-05 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]