Japanese
Home
Search
Horizontal Search
Publication Search
( Advanced Search )
Patent Search
( Advanced Search )
Research Highlight Search
( Advanced Search )
Researcher Search
Search by Organization
Support
FAQ
T2R2 User Registration
Doctoral thesis registration
Support/Contact
About T2R2
What's T2R2?
Operation Guidance
Leaflets
About file disclosure
Related Links
Tokyo Tech
STAR Search
NII IR Program
Home
>
Help
Publication Information
Title
Japanese:
組込みシステム向けFRP言語におけるモデル検査を用いた状態依存動作の検証
English:
Author
Japanese:
内藤博
,
森口草介
,
渡部卓雄
.
English:
Hiroshi Naito
,
Sosuke Moriguchi
,
Takuo Watanabe
.
Language
Japanese
Journal/Book name
Japanese:
情報処理学会研究報告
English:
IPSJ SIG Technical Report
Volume, Number, Page
Vol. 2021-EMB-57 No. 4 pp. 1-2
Published date
June 28, 2021
Publisher
Japanese:
情報処理学会
English:
Conference name
Japanese:
情報処理学会第57回組込みシステム研究会(SIGEMB57)
English:
Conference site
Japanese:
English:
Official URL
http://id.nii.ac.jp/1001/00211595/
Abstract
関数リアクティブプログラミング(FRP)は組込みシステム等のリアクティブシステムを簡潔に記述するための方法である. FRPでは時間変化する値を時変値として表現し,システムをそれらの依存関係に基づいて表現する. 組込みシステムの設計にはしばしば状態遷移モデルが用いられる. モデルの性質はモデル検査を用いて検証できるが,抽象度の違いからその性質を実装(コード)がみたしているか否かを示すのは一般に難しい. XStormは状態遷移モデルを用いて設計された組込みシステムに適した純粋FRP言語であり,状態依存動作を陽に表現するための言語機構を備えている. 本研究ではXStormで記述されたプログラムから状態遷移モデルを抽出してモデル検査器Spinを用いて検証する方法を提案し,例題の記述および検証を通してその有効性について議論する. 本手法で抽出されたモデルは設計モデルに近く,比較的抽象度の高い性質の検証が可能になる.
©2007
Tokyo Institute of Technology All rights reserved.