@techreport{oai:ipsj.ixsq.nii.ac.jp:00211701,
 author = {内藤, 博 and 森口, 草介 and 渡部, 卓雄},
 issue = {4},
 month = {Jun},
 note = {関数リアクティブプログラミング（FRP）は組込みシステム等のリアクティブシステムを簡潔に記述するための方法である．FRP では時間変化する値を時変値として表現し，システムをそれらの依存関係に基づいて表現する．組込みシステムの設計にはしばしば状態遷移モデルが用いられる．モデルの性質はモデル検査を用いて検証できるが，抽象度の違いからその性質を実装（コード）がみたしているか否かを示すのは一般に難しい．XStorm は状態遷移モデルを用いて設計された組込みシステムに適した純粋 FRP 言語であり，状態依存動作を陽に表現するための言語機構を備えている．本研究では XStorm で記述されたプログラムから状態遷移モデルを抽出してモデル検査器 Spin を用いて検証する方法を提案し，例題の記述および検証を通してその有効性について議論する．本手法で抽出されたモデルは設計モデルに近く，比較的抽象度の高い性質の検証が可能になる．},
 title = {組込みシステム向けFRP言語におけるモデル検査を用いた状態依存動作の検証},
 year = {2021}
}