SIGEMB57 Talks

Posted on June 28, 2021

関数リアクティブプログラミングにおける時変値の初期値の自動決定

白鳥佑弥, 森口草介, 渡部卓雄
情報処理学会第57回組込みシステム研究会(SIGEMB57)，オンライン開催，2021年6月28日．

概要

関数リアクティブプログラミング(FRP)は，時間とともに変化する値を時変値として抽象化することで，組込みシステム等のリアクティブシステムを時変値の更新計算として記述するプログラミングパラダイムである． 時変値の変化量や累積値，およびシステムの状態等を表現するためには時変値の過去の値を参照する必要があるが，システム起動時には過去の値は存在しないため，あらかじめ初期値を設定する必要がある． センサの計測値や現在時刻等，実行時に決定される値について不適切な初期値を用いた場合，システム起動直後の挙動が不安定になることがある． アプリケーションごとに適当な値を想定して初期値とするといったアドホックな方法は，プログラムのモジュール化を阻害する． 本研究では組込みシステム向けFRP言語の時変値について，適切な初期値を自動的に決定する手法について提案する．

関数リアクティブプログラミング言語のための時間制約付きイベントの記述方式

堀紗知子, 森口草介, 渡部卓雄
情報処理学会第57回組込みシステム研究会(SIGEMB57)，オンライン開催，2021年6月28日．

概要

本研究では，小規模組込みシステム向け関数リアクティブプログラミング言語Emfrpにおいて時間制約のあるイベントを検出する際の記述方式を提案する． 例えばボタンを短く1回押す，ダブルクリックする，長押しするといった，ある事象が時間制約付きで複数回発生するようなイベントを検出することを考える． イベントに含まれる事象の回数を変更したり，同じ事象を観察する異なるイベントを区別して検出しようとすると，コードが複雑化し，かつ既存のコードへの変更が必要になる． このような問題の解決を目的とした時間制約付きイベントの記述方式と，その記述からEmfrpのコードを生成する手法を提案する． 例題の記述を通して提案手法を利用したときの定義や変更のしやすさについて議論する．

組込みシステム向けFRP言語におけるモデル検査を用いた状態依存動作の検証

内藤博, 森口草介, 渡部卓雄
情報処理学会第57回組込みシステム研究会(SIGEMB57)，オンライン開催，2021年6月28日．

概要

関数リアクティブプログラミング(FRP)は組込みシステム等のリアクティブシステムを簡潔に記述するための方法である． FRPでは時間変化する値を時変値として表現し，システムをそれらの依存関係に基づいて表現する． 組込みシステムの設計にはしばしば状態遷移モデルが用いられる． モデルの性質はモデル検査を用いて検証できるが，抽象度の違いからその性質を実装（コード）がみたしているか否かを示すのは一般に難しい． XStormは状態遷移モデルを用いて設計された組込みシステムに適した純粋FRP言語であり，状態依存動作を陽に表現するための言語機構を備えている． 本研究ではXStormで記述されたプログラムから状態遷移モデルを抽出してモデル検査器Spinを用いて検証する方法を提案し，例題の記述および検証を通してその有効性について議論する． 本手法で抽出されたモデルは設計モデルに近く，比較的抽象度の高い性質の検証が可能になる．