2026-03-07T07:06:04Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00235692 2025-01-19T09:33:30Z 6504:11678:11697

リアクティブシステム仕様の検証における単純な反例の導出 阿部, 遥斗 島川, 昌也 ソフトウェア科学・工学 リアクティブシステムの仕様の安全性を確かめるために数学的技法を用いた形式検証に注目が集まっている．形式検証を用いて仕様に欠陥が存在するか判定できる．もし欠陥があれば，仕様を修正しなくてはならない．修正には，判定で得られる反例が利用される．その際に反例は単純な方が効率的に修正を行える．しかし，既存の反例導出ツールでは必ずしも単純な反例が導出されるとは限らない．本研究では，理解のしやすさ向上と機械的な修正サポートの効率化のための単純な反例を導出する手法の提案とその実装を行う．仕様から全ての反例を表現する無限木オートマトンを構成し，SATソルバを用いて解析していくことで単純な反例を導出する． conference paper 情報処理学会 2024-03-01 application/pdf 第86回全国大会講演論文集 1 2024 165 166 AN00349328 https://ipsj.ixsq.nii.ac.jp/record/235692/files/IPSJ-Z86-2K-02.pdf jpn