WEKO3
アイテム
組込みシステム向けFRP言語におけるモデル検査を用いた状態依存動作の検証
https://ipsj.ixsq.nii.ac.jp/records/211701
https://ipsj.ixsq.nii.ac.jp/records/211701fa31bcf5-b49d-4452-996a-4cbeb00b1c5d
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-EMB21057004.pdf (776.2 kB)
|
Copyright (c) 2021 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2021-06-21 | |||||||||||
| タイトル | ||||||||||||
| タイトル | 組込みシステム向けFRP言語におけるモデル検査を用いた状態依存動作の検証 | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | プログラミング言語 | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||
| 資源タイプ | technical report | |||||||||||
| 著者所属 | ||||||||||||
| 東京工業大学情報理工学院情報工学系 | ||||||||||||
| 著者所属 | ||||||||||||
| 東京工業大学情報理工学院情報工学系 | ||||||||||||
| 著者所属 | ||||||||||||
| 東京工業大学情報理工学院情報工学系 | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Department of Computer Science, School of Computing, Tokyo Institute of Technology | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Department of Computer Science, School of Computing, Tokyo Institute of Technology | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Department of Computer Science, School of Computing, Tokyo Institute of Technology | ||||||||||||
| 著者名 |
内藤, 博
× 内藤, 博
× 森口, 草介
× 渡部, 卓雄
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 関数リアクティブプログラミング（FRP）は組込みシステム等のリアクティブシステムを簡潔に記述するための方法である．FRP では時間変化する値を時変値として表現し，システムをそれらの依存関係に基づいて表現する．組込みシステムの設計にはしばしば状態遷移モデルが用いられる．モデルの性質はモデル検査を用いて検証できるが，抽象度の違いからその性質を実装（コード）がみたしているか否かを示すのは一般に難しい．XStorm は状態遷移モデルを用いて設計された組込みシステムに適した純粋 FRP 言語であり，状態依存動作を陽に表現するための言語機構を備えている．本研究では XStorm で記述されたプログラムから状態遷移モデルを抽出してモデル検査器 Spin を用いて検証する方法を提案し，例題の記述および検証を通してその有効性について議論する．本手法で抽出されたモデルは設計モデルに近く，比較的抽象度の高い性質の検証が可能になる． | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AA12149313 | |||||||||||
| 書誌情報 |
研究報告組込みシステム（EMB） 巻 2021-EMB-57, 号 4, p. 1-2, 発行日 2021-06-21 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-868X | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
