Home >

news ヘルプ

論文・著書情報


タイトル
和文:組込みシステム向けFRP言語におけるモデル検査を用いた状態依存動作の検証 
英文: 
著者
和文: 内藤博, 森口草介, 渡部卓雄.  
英文: Hiroshi Naito, Sosuke Moriguchi, Takuo Watanabe.  
言語 Japanese 
掲載誌/書名
和文:情報処理学会研究報告 
英文:IPSJ SIG Technical Report 
巻, 号, ページ Vol. 2021-EMB-57    No. 4    pp. 1-2
出版年月 2021年6月28日 
出版者
和文:情報処理学会 
英文: 
会議名称
和文:情報処理学会第57回組込みシステム研究会(SIGEMB57) 
英文: 
開催地
和文: 
英文: 
公式リンク http://id.nii.ac.jp/1001/00211595/
 
アブストラクト 関数リアクティブプログラミング(FRP)は組込みシステム等のリアクティブシステムを簡潔に記述するための方法である． FRPでは時間変化する値を時変値として表現し，システムをそれらの依存関係に基づいて表現する． 組込みシステムの設計にはしばしば状態遷移モデルが用いられる． モデルの性質はモデル検査を用いて検証できるが，抽象度の違いからその性質を実装（コード）がみたしているか否かを示すのは一般に難しい． XStormは状態遷移モデルを用いて設計された組込みシステムに適した純粋FRP言語であり，状態依存動作を陽に表現するための言語機構を備えている． 本研究ではXStormで記述されたプログラムから状態遷移モデルを抽出してモデル検査器Spinを用いて検証する方法を提案し，例題の記述および検証を通してその有効性について議論する． 本手法で抽出されたモデルは設計モデルに近く，比較的抽象度の高い性質の検証が可能になる．

©2007 Tokyo Institute of Technology All rights reserved.