日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

組込みシステム向け FRP 言語におけるリアルタイムタ
スクの記述と処理機構
十河 健人

森口 草介

渡部 卓雄

関数リアクティブプログラミング（FRP）は，時間と共に変化する値である時変値を宣言的に組み合わせることによってリアクティブシステムを記述するプログラミングパラダイムである．組込みシステム向け FRP 言語である
EvEmfrp は，時変値に対しその更新タイミングを型情報として持たせることで周期的・非周期的なタスク処理を記述することができる．しかし，それぞれの時変値の更新がいつ完了するかといった実時間性に関する保証がなく，リアルタイムシステム向けの言語としては十分ではない．本研究では，EvEmfrp をもとに，リアルタイムシステムを記述するための構文を備えた FRP 言語を提案する．本言語では，明示的にタスクとそのデッドラインを記述することができ，各タスクでどの時変値が更新されるかを時変値が持つタイミングから静的に決定することができる．また，本言語におけるタスク処理に適したスケジューリング機構を提案する．

し周期的・非周期的なタスクを記述できるように拡張

1 はじめにした言語として，EvEmfrp [14] がある．この言語でリアクティブシステムは外部からの入力に対して応は，時変値ごとにその更新タイミングを型情報として答を行うシステムであり，Web アプリケーションな持たせることでそのようなタスクの記述を可能とし

どの GUI や組込みシステムなどが該当する．リアクている．しかし，それぞれの時変値の更新が完了する

ティブシステムを手続き型の手法で記述する場合は時刻に対する保証がないため，タスクの実時間性が求ポーリングやコールバックなどが用いられてきたが，められるリアルタイムシステムには適していない．

これらの手法を用いるとプログラムが煩雑になりや

Priority-based FRP（P-FRP） [12] は，時変値のすいという問題がある [2]．

更新イベントに優先度を導入することで実時間性の関数リアクティブプログラミング（Functional

考慮を可能とした FRP の派生モデルである．P-FRP

Reactive Programming，FRP） [10] はリアクの特徴はそのスケジューリング方式である．多くのリティブシステムを記述するプログラミングパラダイム

アルタイムシステムでは，タスクの実行中に他の優であり，時間と共に変化する値である時変値を宣言的

先度の高いタスクが割り込んで（プリエンプトして）に組み合わせることによってシステムを簡潔に記述す実行できるプリエンプティブスケジューリングが用いることができる．

られ，一般的にはプリエンプトされたタスクは中断

Emfrp [13] は小規模組込みシステム向け FRP 言語

した地点から再開することができる．一方 P-FRP でである．マイクロコントローラなどリソースが限られは，時変値同士の関係の一貫性を保つため，プリエンた環境で動作させるため，メモリの使用量を静的に見プトされたタスクが再開する際に最初からタスクを積もることができるなどの特徴を持つ．Emfrp に対やり直すという実行モデルが提案された．しかし，こReal-time Task Description and Processing Mechanism in FRP Language for Embedded Systems
Kento Sogo, Sosuke Moriguchi, Takuo Watanabe, 東京工業大学, Department of Computer Science, Tokyo
Institute of Technology.

のモデルはその性質上タスクの実行が非効率になるという問題がある．
本研究では，EvEmfrp をもとにしたリアルタイム
システム向け FRP 言語である FreacTime を提案する．特徴として明示的に個々のタスクとそのデッドラ

ントを発行する時刻を表すものであり，実際に更新がインを記述することができ，各タスクでどの時変値が開始または完了する時刻に対する保証をするもので更新されるかを時変値が持つタイミングから静的にはない．そのため，実時間性の保証を必要とするリア

決定することができる．また，FreacTime における

ルタイムシステム向けの言語としては十分ではない．

タスクモデルに適したスケジューリング機構を提案

Priority-based FRP（P-FRP） [12] は FRP に優する．

先度を導入したモデルである．Abort-and-Restart

本論文は以下のように構成される．まず 2 節で本（AR）モデルは P-FRP 向けの実行モデルであり，あ研究の動機について述べる．次に 3 節で FreacTime

るタスクが実行中に他の優先度の高いタスクがプリエの言語機能について説明し，4 節でそれらを形式化す

ンプトして実行する場合，プリエンプトされたタスク

る．5 節では FreacTime のタスクスケジューリング

が再開する際に最初から実行をやり直すという実行モ

機構を説明する．そして 6 節で関連研究について述デルである．このモデルにより時変値間の一貫性を保べ，最後に 7 節で本研究のまとめと今後の課題につちながらタスクのプリエンプションが可能となるが，いて述べる．

タスクのやり直しが発生するという性質上実行の効率が悪い．一方，P-FRP であってもタスクで行われ2 研究の動機る処理によっては一般のプリエンプティブスケジュー

リアルタイムシステムとは，それが行う処理（タスリングのように中断した地点から再開できる場合もク）に対して完了までの期限（デッドライン）が設定ある．例えば，タスク同士が互いに独立している，つされたシステムである．期限までに処理が終わらな

まりタスクの実行に関わる時変値が全く異なる場合

かった場合に壊滅的な被害をもたらすようなシステム

はプリエンプションが起こってもタスクの再開時に最をハードリアルタイムシステムと呼び，航空機システ

初からやり直す必要がない．しかし，そのような状況

ム，自動車システムや原子力発電所制御システムなを考慮した実行モデルの議論は行われていない．

どが該当する．これらのシステムでは時間的な保証

そのため本研究では，既存の組込みシステム向けのほか，システムの機能の正しさや信頼性も重要で

FRP 言語をもとにしてリアルタイムシステム向け

ある [1]．FRP のような宣言的なプログラミング手法

FRP 言語を設計し，タスク同士の独立性を形式的には，副作用の分離などを通してプログラムの予測可能

表現し，それを用いたスケジューリング機構を提案

性を高めることができるため，リアルタイムシステム

する．

のような信頼性が求められるシステムに適していると考える．

3 FreacTime

EvEmfrp [14] は組込みシステム向けの FRP 言語で

FreacTime は本研究で提案するリアルタイムシ

あり，時変値に自身の更新タイミングを持たせること

ステム向け FRP 言語である．この言語は Emfrp をで周期的・非周期的な処理を記述できる．EvEmfrp のベースにし，EvEmfrp の要素を取り入れながら，リ

課題として，実時間性の保証があげられる．EvEmfrp

アルタイムシステム向けに明示的なタスクの記述とのランタイムにおいて，時変値が持つ更新タイミング

そのデッドラインの設定ができるように設計された言に対応するのはタイマー割り込みや外部割り込みであ語である．本節では FreacTime の言語機能についてる．それらの割り込みハンドラでは，どの時変値を更説明する．

新するべきかを表すイベントをイベントキューに送信
する．そしてメインタスクと呼ばれる処理でイベント

3. 1 サンプルコード

キューからイベントを取り出し，その時変値を更新す

FreacTime のサンプルコードを図 1 に示す．このる処理を行う．つまり，時変値が持つ更新タイミング

プログラムは簡易的な自動ドア制御システムを記述

はその時変値を更新するべきであることを表すイベしたものである．通行人を検知するセンサーが前後

に 2 つあり（sensor1，sensor2），これらの状態とイミングが’ controlであるため closedもタイミング

ドアの開閉状態（pos）に応じてドアをどう動かすか’ controlをもつ．状態ノードには初期値を設定する（direction）を決める．また，障害物を検知するセことができ，初期値を持つノードは@lastを用いて過ンサーもあり，ドアが閉じている状態で障害物を検知

去に更新された時の値を参照することができる．例えした場合はドアを開くように制御する．この制御は人ば 17 行目のノード startClosingはノード openの現などが挟まれることを防ぐためのもので，実時間性が在の値と過去 2 回の値を用いて定義されており，ドア求められる．

が開いている状態を 3 回確認した時にドアを閉じる

以降，このサンプルコードを例に FreacTime の言ように制御するということを表現している．

語機能について説明する．

3. 3 タイミング
3. 2 時変値

ノードはそれぞれタイミングを持つと説明してきEmfrp と同様に FreacTime における時変値はノーた．このタイミングは，具体的には定数であることをドと呼ばれる．ノードには入力ノードと状態ノードの表す const か，入力タイミングか入力タイミングの列

2 種類がある．

で表される．例えば 8 行目の maxPosのタイミングは

入力ノードはキーワード inに続いて宣言される

const であり，後に説明するが 11 行目の activateはノードであり，外部からの入力を値とする時変値であ

入力タイミングの列 ’sensor1 | ’sensor2をタイミン

る．例題では，sensor1，sensor2，control，pos，

グとして持つ．タイミングはどの入力時変値と同時にobstacleが入力ノードである．その中で例えば 2，3更新されるかを表す．例えば activateは sensor1ま行目の sensor1と sensor2は，それぞれドアの前後

たは sensor2が更新された時に同時に更新される．

に設置されたセンサーからの入力を値とする．入力
ノードはそれぞれ入力タイミングという情報を持つ．

3. 4 式

入力タイミングは外部からの入力を受け取るタイミン

ノードの定義には二項演算や if 式などのを用いグを抽象化したものであり，具体的なタイミングは後ることができる．このような式を基本式と呼ぶ．二述のタスクによって指定される．入力ノードのタイミ

項演算などで異なるタイミングを持つノードを組

ングは，そのノードの宣言でデータ型以外に何も指定

み合わせる場合，その式のタイミングはそれぞれのされていない場合はノード名に「’ 」をつけたものでタイミングを合成したようなタイミングになる．例

表現される．例えば，sensor1は’ sensor1という入力

えば activateの定義式となっている sensor1 ||タイミングを持つ．一方 5 行目の posのようにデータ

sensor2は，sensor1と sensor2のタイミングを合成型の後にタイミングが指定されている場合はそのタした’ sensor1 | ’sensor2を持つ（そのため activate

イミングを持つ．また，4 行目，6 行目のようにデーのタイミングも’ sensor1 | ’sensor2となる）．

タ型として Unitが指定されているものがある．これ

when q { e }の形で記述される式を when 式と呼ぶ．

は外部からの入力を受け取らないが，ある種のイベン

q はタイミングアノテーションと呼ばれるもので，こトとしてタイミングだけを使うために定義される．

こでは when 式の評価が行われるタイミングを指定

状態ノードはキーワード nodeに続いて定義される

する．例えば 24 行目の when 式は，25 行目から 29

ノードであり，システムの中間状態を表す時変値であ行目までの式をタイミング’ controlに評価する式でる．例題では，maxPos，minPos，activate，closed

ある．

，open，closing，startClosing，directionが状態@@はタイミング和と呼ぶ演算子で，@@の前の式が評ノードである．状態ノードもタイミングをもち，これ価されるタイミングではその式が，そうでない場合ははノード同士の依存関係によって導出される．例え

後の式が式全体の結果になる．例えば，directionのば 13 行目の closedは posに依存しており，posのタ

値はタイミング’ obstacleでは 22，23 行目を評価し1

module AutomaticDoorControl

2

in sensor1 : Bool,3

sensor2 : Bool,

4

control : Unit,

27

else if startClosing then -1

28

else if open then 029else direction@last[1]

30

}

31
5

pos

6

obstacle : Unit

: Int ’control,
32

init ’sensor1[sensor1=false],

33’sensor2[sensor2=false],

34’control[pos=0]

78node maxPos = 100

9node minPos = 0

3536

task checkActSensor1 = periodic(0s, 500ms) {

10
11

37

in ’sensor1

38

deadline 500ms

node activate = sensor1 || sensor2

12
13

39

}

40

task checkActSensor2 = periodic(0s, 500ms) {node closed = pos == minPos

14

node init[false, false] open = pos == maxPos

15

node closing = direction@last[1] < 0

in ’sensor2

41

deadline 500ms

42
16
17
18

43

}

44

task controlDoor = periodic(0ms, 200ms) {node startClosing = open@last[2] &&open@last[1] && open
45

in ’control

46

out direction

19
20# 0: stop, 1: open, -1: close

21

node init[0] direction = when ’obstacle {deadline 200ms

47

22

if closing then 1

23else direction@last[1]

48

}

49

task detectObstacle = interrupt(500ms) {in ’obstacle

50
24
25
26

} @@ when ’control {51

out direction

52

deadline 100ms

if activate then if open then 0 else 1
else if closed then 0
53

図1

}

AutomaticDoorControl.frtm

た値に，タイミング’ controlでは 25 行目から 29 行

ワードを用いて初期化子を記述することでノードの初目までを評価した値になる．

期値を設定することができる．コード例では 32 行目
から 34 行目までで入力ノードを初期化している．こ3. 5 初期化子の時，初期化されたノードに依存するノードも定義式

状 態 ノ ー ド activateは タ イ ミ ン グ’ sensor1 |に従って初期化される．

’sensor2を持つと説明した．ここで，最初に sensor1
が更新され，その時にまだ一度も sensor2が更新され

3. 6 タスクていないような場合を考える．この時，sensor2の値

ノードはそれぞれタイミングを持つが，これはどのはまだ定まっていないため，activateの値も定まら

入力ノードが更新された時に自身も更新されるのかなくなってしまう．このように，ある時変値がそれがということを表す抽象的な情報である．どのノードが更新されないタイミングで参照される場合に値がまだ具体的にいつ更新されるのかは，タスクとして記述さ定まっていないような状態を避けるために，initキー

れる．

タスクが実行される具体的な時刻はイベントによっ注意点としては，@@はノード定義のトップレベルて指定される．イベントは 3 種類あり，まず periodic

でのみ記述でき，when式も二項演算などの部分式と(t, t′ )は開始時刻 t，周期 t′ の周期的イベントを表して記述することはできない．これは，タイミングにす．たとえば，36 行目のタスク checkActSensor1は関する意味論を明確にするためである．例えばそれぞ

periodic(0s, 500ms)となっており，通行人を検知れ異なるタイミングをもつノードを用いて (a @@ b)

するセンサーを 500ms ごとにチェックするタスクと定+ cという式が書けた場合，cが更新されるタイミン

義されている．interrupt(t)は外部割り込みによるグでは aと bのどちらを参照すべきかが曖昧になって散発的イベントを表し，t はイベントの発生の最小イン

しまう．

ターバルを表す．４９行目のタスク detectObstacleのイベントは外部割り込みのイベントとなっており，

4. 2 タイミングの形式化

障害物を検知するセンサーが障害物を検知した時にタイミングは図 4 のように定義される．ノードのタ発生する．最後に event(τ ->t)はタスク τ から時刻

イミング Θ は，定数であることを示す const か，入t 後に発生する内部イベントを表す．

力ノードのタイミング θ の列 θ1 , . . . , θm で表される．

タスクにおいてどのノードが更新されるかは，inに

このとき，それぞれ同じ入力タイミングで構成される

続いて記述されるタイミングアノテーションで指定さが並び順が異なるような 2 つのタイミングは同じタれる．例えば，タスク controlDoorではタイミング

イミングとみなす．

’controlが指定されている．そのためまずタイミング∈Θ は入力タイミング θ がタイミング Θ に含まれ’ controlを持つ入力ノード posが更新され，その後タることを表す．vΘ はタイミングに関する半順序関係

イミング’ controlを持つ状態ノードである closedやであり，タイミング Θ1 がタイミング Θ2 に含まれる

directionなどが更新される．outに続いて記述されことを表す．merge は複数のタイミングを合成する関ているノードは，タスクの最後に外部へ出力するノー数である．例えば，merge{θ1 | θ2 , θ3 } = θ1 | θ2 | θ3ドを表す．deadlineキーワードはタスクのデッドラである．この merge 関数は，タイミングの半順序関

インを指定する．

係 vΘ における上限として定義することができる．

例題における各タスクの動作は 2 のようになる．

それぞれのノードがどのタイミングを持つかという情報を持つものをタイミング環境と呼び，Γ で表す．

4 形式化
3 節では本研究で提案する言語 FreacTime の機能を説明した．本節では FreacTime の形式化を行う．
この形式化は，5 節でスケジューリングについての議論を行うために必要となる．

タイミング環境 Γ の導出は以下の手順で行われる．

1. すべての状態ノード ns に対して Γ(ns ) = constとなるように Γ を初期化する．

2. 入力ノードのタイミングを求める．入力ノード
ni が ni : ρ と定義されている場合は，ni のタイ

まず最初に FreacTime の構文を定義する．そしてミングは ’ni ，つまり Γ(ni ) = ’ni となるよう Γ

次にタイミングの定義とそれぞれのノードが持つタを更新する．ni が ni : ρ ’niq と定義されている

イミングの導出について述べる．その後，依存・参照場合，niq が niq : ρ ∈ I と定義されているなら関係という概念を導入する．これはノード間の関係

Γ(ni ) = ’niq とし，そうでない場合はタイミングを表すもので，タスクの形式化のために必要となる．

エラーとする．

最後に個々のタスクがどのように実行されるかを形式的に定義する．

3. ノード同士の依存関係から有向グラフを構築する．この時，ノード ns の更新式に現れる式の種類によって以下のように依存関係を定義する．

4. 1 構文FreacTime の構文は図 3 のように定義される．

• when q { eb }の場合，ns は q で指定された入力ノードに依存するとする．

図2

図 1 のタスクの動作

StateNode3

ns

InputNode3

ni

Variable3x

Literal3lFunction3f

UnaryOp

3

uop

BinaryOp

3

bopConstrLabel

3

C

DataType

3

ρ

Time

3

t

Task

3

τ

Module

3

M

Node

3

n

::= n | ns

TimingAnnotation

3

q

Expression

3e

WhenExpression

3

BasicExpresison

3

i

::=

’ni1 |. . . |’nim::=

ew | e @@ ew

e

w

::=

eb | when q { eb }

e

b

::=

l | x | n | ns @last[l] | uop eb | eb1 bop eb2|

f (eb1 , . . . , ebm ) | C(e1 , . . . , em ) | if eb1 then eb2 else eb3|

case eb of p1 -> eb1 , . . . , pm -> ebm

Pattern3

p::=C(x1 , . . . , xm )

Event

3

ϵ

::=

periodic(t1 , t2 ) | interrupt(t) | event(τ ->t)M::=

module M in I F N

I::=∅ | I, n : ρ | I, n

F::=

∅ | F , fun f (x1 , . . . , xm ) = eb

N::=

∅ | N , node n = e | N , node init[e1 , . . . , em ] n = e(node deﬁnitions)

Init

::=

∅ | Init, ’ni | Init, ’ni [ni1 =l1 , . . . , nim =lm ](initializer deﬁnitions)::=∅ | T , task τ = ϵ {(task deﬁnitions)

T

i

i

init Init T(module deﬁnition): ρ ’niq(input node declarations)(function deﬁnitions)ssin q out ns1 , . . . , nsm deadline t }図3

FreacTime の構文

InputTiming

3

θ

::=

’ni

(ni ∈ {ni | ni :ρ ∈ I})

Timing

3

Θ

::=
|

θ1 | · · · | θmconst(m ≥ 1)∈Θ={(θ, Θ) | ∃θ1 , . . . , θm .(Θ = θ1 | · · · | θm ∧ ∃i.θi = θ)}vΘ={(Θ1 , Θ2 ) | ∀θ.(θ ∈Θ Θ1 ⇒ θ ∈Θ Θ2 )}merge{Θ1 , . . . , Θm }=sup{Θ1 , . . . , Θm }

Γ:Node → Timing
図4(タイミング環境)

タイミングの定義• それ以外の場合，ns は@lastによる参照を

ラ フ を た ど り 到 着 可 能 な ノ ー ド ns に 対 し て含みその式に現れるノードに依存するとする．

Γ(ns ) = merge{Γ(ns ), Γ(ni )} となるよう Γ を

4. ある入力ノード ni について，ni から依存グ更新する．この操作を ni から到着可能なノード

全てに対して行う．

5. 4 をすべての入力ノードに対して逐次的に行う．

r以降 Γ はこの手順によって導出されたタイミング環
境を指す．

4. 3 依存・参照関係::=(θ, N d , N l , N r )

N

d

:

依存ノード

N

l

:

直前値参照ノード

Nr

:

参照ノード

δ

::=

∅ | δ, r∆::=∅ | ∆, ns 7→ δ

それぞれ異なるタイミングをもつノード a，b を用

図5(依存・参照ノード群)(依存・参照環境)

依存・参照関係

いて，ノード c が

c=a+b

nodes(eb ) は基本式 eb の中に現れるノードの集合をと定義されているとする．a が更新された時，c は a得る関数であり，nodeslst (eb ) は eb の中で@last参の変化に応じて更新される．この時，c は a だけでな

照されるノードの集合を得る関数である．これらはく b も定義に用いられているため，c は変化した a の基本式の構造から帰納的に定義することができる．

値と b の現在の値を用いて更新される．このような場

timing(eb , Γ) は基本式 eb のタイミングを求める関合，c は a に依存して変化し，その時 b を参照してい数であり，timingq (q, I) はタイミングアノテーショ

ると考えることができる．このように，ノード間の関ン q が表すタイミングを求める関数である．そして係には依存関係の他に参照関係も存在する．

RelJeK(I, Γ) は式 e に対する依存・参照ノード群 δ をノード間の関係は，• そのノードの変化に自身が依存しているという関係を表す依存，• そのノードの直前値を参照しているという関係を表す直前値参照，• そのノードの値を参照しているという関係を表す参照

求める関数である．
これらの関数を用いて，ノード定義 N に対する依存・参照環境 ∆ は，∆ = {ns 7→ RelJeK(I, Γ) | ns =e ∈ N ∨ node init[e1 , . . . , em ] = e ∈ N } と導出される．以降 ∆ はこのようにして導出された依存・参照環境を指すものとする．
依存・参照関係を用いてラベル付き有向グラフを構の 3 つの関係で定義される．ただし直前値の参照は

築すれば，システムのタイミング毎のノード間の依存@lastによる参照のことを指す．これらの関係はタイ関係を視覚的に表現することができる．また，依存・ミングによって変化する．先ほどの例では，a が更新

参照関係は次の 4. 4 節でタスクの形式的な定義にもされるタイミングでは c は a に依存し b を参照して用いる．

いるが，b が更新されるタイミングでは c は a を参照
し b に依存している．このようなノード間の関係を依存・参照関係と呼び，図 5 のように定義する．

4. 4 タスクの形式化
タスクは外部からの入力を受け取り，それに依存すr はあるノードに対しての特定のタイミング θ におるノードを更新し，特定のノードの値を外部へ出力す

ける依存・参照関係を表し，タイミング θ，その時のる処理とみなすことができる．これを形式的に表すと依存ノード，直前値参照ノード，参照ノードの 4 つ組

図 7 のようになる．以降，これについて詳しく説明で表される．依存・参照ノード群 δ は r の集合で表する．

され，あるノードに対してそれぞれのタイミングでまず，タスクにおいて行われる処理に関係する

どのようなノードと依存・参照関係を持つかを表す．

ノードについて整理する．どの入力ノードの値を依存・参照環境 ∆ は全てのノードに対する依存・参外部から受け取るかは，タイミングアノテーショ

照関係を表し，ノードから依存・参照ノード群への写

ン q によって決まる．q で指定されたタイミング像として表現される．

を Θτ とすると，Θτ = timingq (q, I) である．そし依存・参照関係の導出のための関数を図 6 に示す．

て，更新するべき入力ノードの集合を Iτ とすると，

nodes(eb ):eb の中に現れるノードの集合を得る関数

nodeslst (eb ):eb の中で @last参照されるノードの集合を得る関数

timing(e , Γ)=timingq (’ni , I)=

merge{Γ(n) | n ∈ (nodes(eb ) ∪ nodeslst (eb ))}′ ni if ∃ρ.ni :ρ ∈ I

timingq (’ni1 |. . . |’nim , I)=b

RelJe @@ ew K(I, Γ)′ niqif ∃ρ, ρ′ .(ni :ρ ’niq ∈ I ∧ niq :ρ′ ∈ I)

merge{timingq (’ni1 , I), timingq (’ni2 |. . . |’nim , I)}=δ ∪ {r | r ∈ RelJew K(I, Γ) ∧ ∀r′ ∈ δ.π1 (r) 6= π1 (r)}={(θ, N d (θ), N l (θ), N r (θ)) | θ ∈Θ Θ}

where δ = RelJeK(I, Γ)
RelJwhen q { e }K(I, Γ)
where

Θ

=

timingq (q, I)

d

N (θ)

=

{n | n ∈ nodes(e) ∧ θ ∈Θ Γ(n)}N l (θ)={ns | ns ∈ nodeslst (e) ∧ θ ∈Θ Γ(n)}N r (θ)={n | n ∈ (nodes(e) ∪ nodeslst (e)) ∧ (θ ∈Θ Γ(n) ∨ Γ(n) = const)}

RelJe K(I, Γ)
b

where

=

{(θ, N d (θ), N l (θ), N r (θ)) | θ ∈θ Θ}=timing(eb , Γ)N d (θ)={n | n ∈ nodes(eb ) ∧ θ ∈Θ Γ(n)}

l

N (θ)

=

{ns | ns ∈ nodeslst (eb ) ∧ θ ∈Θ Γ(n)}N r (θ)={n | n ∈ (nodes(eb ) ∪ nodeslst (eb )) ∧ (θ ∈Θ Γ(n) ∨ Γ(n) = const)}Θ

図6

依存・参照関係の導出である．これを形式的に表すと，{n | ∃ns ∈ Uτ .∃δ ∈Iτ = {ni | Γ(ni ) vΘ Θτ } となる．
次に，更新するべき状態ノードを考える．これ∆(ns ).∃r ∈ δ.π1 (r) ∈Θ Θτ ∧ n ∈ π3 (r)} \ (Iτ ∪ Uτ )らは更新された入力ノードに依存するノードであとなる．よって参照ノードの集合 Rτ はこれらの和集

るが，タスクのタイミング Θτ によって求められ合となる．

る．更新するべき状態ノードの集合を Uτ とすると，

Uτ = {n | ∃θ ∈Θ Θτ .θ ∈Θ Γ(n )} となる．
ss

状態ノードの更新には，入力ノード以外にも状態ノードの更新式で参照されているノードも必要である．これらは，直前値を参照されるノードと，q に外部に出力するノードの集合 Oτ は，タスクに記述されたノードの集合なので Oτ = {ns1 , . . . , nsm } となる．
次に，タスクで行われる処理を形式的に表現する．
タスクの実行は以下の 5 つのフェーズからなる．

よって指定されたタイミングを持たない参照ノード

1. 入力フェーズの集合であり，依存・参照関係 ∆ によって求めるこ

2. コピーフェーズとができる．まず直前値を参照するノードは，更新

3. 更新フェーズ

するべきノードの集合 Uτ のうちのいずれかのノード

4. 書き戻しフェーズの更新式で，タイミング Θτ で直前値参照されるノー5. 出力フェーズドの集合なので，{n | n∈ Uτ .∃δ ∈ ∆(n ).∃r ∈入力フェーズでは，外部から入力を受け取り新たなδ.π1 (r) ∈Θ Θτ ∧ n = π2 (r)} となる．次に，参照

入力ノードの状態を得る．ここでは状態は，ノードかノードの集合を求める．これは，Uτ のうちのいずれ

らそれが取りうる値への写像として表現する．入力

かのノードの更新式で，タイミング Θτ で参照される

ノードの状態を στi : Iτ → V （V はノードが取りう

ノードのうち，タスク τ で更新されないノードの集合

る値の集合）とし，外部から入力を受け取る関数を

s

s′

s′

s

task τ = ϵ { in q out ns1 , . . . , nsm deadline t }最後に，出力フェーズでは，出力ノードの状態をΘτ=timingq (q, I)

外部に出力する．出力ノードの状態を στo : Oτ → V

Iτ

={ni | Γ(ni ) vΘ Θτ }とし，出力関数を outputτ とすると，出力フェーズUτ={ns | ∃θ ∈Θ Θτ .θ ∈Θ Γ(ns )}は στo ← {n 7→ σ(n) | n ∈ Oτ }; outputτ (στo ) と表Rτ={ns | ns′ ∈ Uτ .∃δ ∈ ∆(ns′ ).∃r ∈ δ.

せる．

π1 (r) ∈Θ Θτ ∧ ns = π2 (r)}∪({n | ∃ns ∈ Uτ .∃δ ∈ ∆(ns ).∃r ∈ δ.
π1 (r) ∈Θ Θτ ∧ n ∈ π3 (r)} \ (Iτ ∪ Uτ ))Oτ{ns1 , . . . , nsm }=5 スケジューリング
3 節では，FreacTime のプログラムがどのように記述され，個々のタスクがどのように動作するかを述べIτ → Vστr:

Rτ → Vてきた．本節では，リアルタイムシステムで求められUτ → Vστo:Oτ → Vる時間的な制約を満たすためにどのようにタスクを

στi

:

στu

:

σ

:

Node → V

inputτ

:() 7→ στi

updateτ:στi × στr 7→ στuoutputτ:στo 7→ ()協調させるかについて述べる．

5. 1 タスクに関する表記法
本研究は，単一のプロセッサ上で実行される固定優

taskτ = {先度のハードリアルタイムシステムを対象とする．シστi← inputτ ();στr← {n 7→ σ(n) | n ∈ Rτ };στu← updateτ (στi , στr );σ← στi ∪ στu ∪ {n 7→ σ(n) | n 6∈ (Iτ ∪ Uτ )};στo← {n 7→ σ(n) | n ∈ Oτ };ステムは FreacTime のプログラムで定義された m 個のタスクからなり，τ1 , . . . , τm と表記する．この時，各タスクは優先度の高い順に並べられているとする．
タスクは周期的もしくは散発的（非周期的）に何度も実行されるが，それぞれの実行をジョブと呼び，タoutputτ (στo );スク τi の k 番目のジョブを Jik と表記する．タスクは}
図7

いくつかのパラメータによって特徴付けられる．まずタスクの実行

はタスク τi の（最悪）実行時間で，これは Ci と表記

inputτ とすると，入力フェーズは στi ← inputτ () とする．タスクが完了するべき時刻はデッドラインと呼表せる．

ばれ，Di と表記する．そして周期（散発的タスクのコピーフェーズでは，システム全体の状態から参場合はジョブ間の最小インターバル）は Ti と表記す

照ノードの状態をローカルにコピーする．システ

る．また，タスクには優先度が割り当てられており，

ム全体の状態を σ : Node → V ，参照ノードの状

これは Pi と表記する．タスクのスケジューリングの態を στr : Rτ → V とすると，コピーフェーズは

際には，これらのパラメータを考慮して行われる．

στr ← {n 7→ σ(n) | n ∈ Rτ } と表せる．

実行時間 C や周期 T といったパラメータは非負整

更新フェーズでは．新たに得た入力ノードの状態

数値を取るとする．つまり，一つのリアルタイムクと参照ノードの状態から更新するノードの状態を求ロックがあり，そのクロックサイクルを時間の最小単める．更新するノードの状態を στu : Uτ

→ V とし，位としてシステムは動作することとする．

状態ノードの値を更新する関数を updateτ とすると，
更新フェーズは στu ← updateτ (στi , στr ) と表せる．

5. 2 プリエンプティビリティ

書き戻しフェーズでは，新しい入力ノードの状態と更2 節で述べたように，FRP では時変値間の関係に新した状態ノードの値をシステム全体の状態に書き戻

よってシステムを記述するため，マルチタスクを行う

す．これは，σ ← σ ∪στu ∪{n 7→ σ(n) | n 6∈ (Iτ ∪Uτ )}場合には時変値間の一貫性を保つ必要がある．そのと表せる．

ため P-FRP では，Abort-and-Restart（AR）モデル

i

やノンプリエンプティブスケジューリング（Nonpre-

つまり，PS のようにタスクを実行した結果が, AR

emptive Scheduling, NP）を用いてきた．しかしこ

モデルで実行した場合の結果か，NP で実行した場合

れらのモデルは一般のプリエンプティブスケジューリの結果と等しくなることを言う．

ング（Preemptive Scheduling, PS）に比べ，高優先度のタスクがデッドラインミスを犯しやすいという問題がある．
一方，個々のタスクに注目すると，そのタスクでタスク τl が τh に対しプリエンプティブルであることを τl ◁ τh と表記する．

4. 4 節で行ったタスクの形式化をもとに，タスク τlが τh に対しプリエンプティブルであるかどうかは以参照・更新される時変値によってはプリエンプショ

下のように判定できる．

ンされても AR モデルのようにタスクの再開時に定理 1. それぞれのジョブが外部から受け取る入力

最初からやり直す必要がない場合がある．例としが，ジョブに対して定数としてみなせる（ジョブの実て，ソースコード 1 のシステムを考える．タスク

行時間，実行順に依存しない）とする．また，タスク

checkActSensor1は，500ms ごとに通行人が検知さのコピーフェーズと書き戻しフェーズはそれぞれアトれたかを確認し，ノード activateを更新する．このミックに行われるとする．

タスクが実行中にタスク detectObstacleがリリースされたとする．このタスクは障害物センサーが障害物

タスク τl が τh に対しプリエンプティブルなのは以下の場合である．

を検知した場合にリリースされ，ドアが閉じている(i) τh で更新されるノードが τl で参照されない

場合にはノード directionを更新しドアを開くよう(ii) τl で更新されるノードが τh で参照されず，τlに制御する．ノード activateはノード directionの値を参照しておらず，タスク detectObstacleにおけるノード directionの更新はノード activateの値を用いない．そのため，タスク checkActSensor1とタ
スク detectObstacleは互いに独立しており，タスク

checkActSensor1の実行にタスク detectObstacle
がプリエンプとしても，checkActSensor1は中断した地点から再開しても良い．
このように，あるタスク τl が別の高優先度のタス
ク τh にプリエンプトされても良い（再開時に最初からやり直す必要がない）場合，τl は τh に対しプリエ
ンプティブルであると呼ぶことにする．具体的に定義
すると，定義 1. タスク τl がタスク τh に対しプリエンプティブルであるとは，タスク τl のジョブ Jl が実行中に τhのジョブ Jh がプリエンプトし実行を開始し，その後Jh の実行が完了した後に Jl が中断した地点から再開
し実行を完了した場合のシステムの状態が以下のいずれかの場合の状態と等しいことをいう．

• それぞれのジョブを Jl ，Jh の順で逐次的に実行した場合のシステムの状態• それぞれのジョブを Jh ，Jh の順で逐次的に実行した場合のシステムの状態と τh の両方で更新されるノードがない
証明. 4. 4 節の形式化より，タスクは，外界とノード
更新で参照されるノードの状態から，更新すべき入力
ノードと状態ノードの状態への関数としてみなすことができる．つまり，外部からの入力を定数とみなすことができる場合，参照されるノードの状態が同じであればタスクの実行結果も同じである．そのため，
タスク τl のジョブ Jl とタスク τh のジョブ Jh に対し，Jl の実行中に Jh がプリエンプトして実行する場
合と，それぞれのジョブを逐次的に実行する場合のノードの状態を比較する．
ここでは，タスク τl で更新する入力ノードの集合を

Il ，参照するノードの集合を Rl ，更新する状態ノードの集合を Ul とする．同様に，タスク τh について
も Ih , Rh , Uh を定義する．
それぞれのジョブが実行される前のシステムの状態を σ とする．以下の三つの実行について考える．

(a) Jl の実行中に Jh がプリエンプトして実行する．この場合，Jl ，Jh はともに σ をもとに実行される．この時の Jl の実行後のシステムの状態
を σp とする．

(b) それぞれのジョブが Jl ，Jh の順で逐次的に実行する．この場合，まず Jl は σ をもとに実行さける Jh の結果は等しい．しかし，Ul と Uh に共れる．この時の Jl の実行後のシステムの状態を通部分があるため，一方のジョブの更新で他方のσl とする．次に Jh が実行されるが，これは Jl のジョブの更新を上書きする．よって実行の結果を実行後のシステムの状態 σl をもとに実行される．

システムの状態に書き戻す順番はシステムの最

この時の Jh の実行後のシステムの状態を σlh と終的な状態に影響を与えるため σp = σlh とはなする．

らず，この場合は τl が τh に対しプリエンプティ(c) それぞれのジョブが Jh ，Jl の順で逐次的に実ブルでない．

行する．この場合，まず Jh は σ をもとに実行さ(iv) τh で更新されるノードが τl で参照され，τlれる．この時の Jh の実行後のシステムの状態をで更新されるノードが τh で参照される場合．

σh とする．次に Jl が実行されるが，これは Jh

この場合は Jh のコピーフェーズで σ から得るの実行後のシステムの状態 σh をもとに実行されRh の状態と Jl のコピーフェーズで σ から得る

る．この時の Jl の実行後のシステムの状態を σhl

Rl の状態が等しくなく，また Jl のコピーフェーとする．

ズで σ から得る Rl の状態と Jh のコピーフェー

これらの実行について，

ズで σ から得る Rl の状態も等しくないため，(a)(i) τh で更新されるノードが τl で更新されない場と (b)，(c) の実行の結果は異なる．よってこの場

合，つまり (Rl ) ∩ (Ih ∪ Uh ) = ∅ の場合．

合も τl が τh に対しプリエンプティブルでない．

Jl のコピーフェーズで σ から得る Rl の状態と，
Jh の実行後に Jl のコピーフェーズで σh から得る Rl の状態は等しい．そのため (a) における Jl

5. 3 スケジューリング方式の結果と (c) における Jl の結果が等しくなる．

前節で述べたプリエンプティビリティを用いて，よって σp = σhl となり，この場合は τl が τh に

FreacTime におけるスケジューリング方式を以下の対しプリエンプティブルである．

ように提案する．

(ii) τl で更新されるノードが τh で参照されず，τlと τh の両方で更新されるノードがない場合，つまり (Rl ) ∩ (Ih ∪ Uh ) = ∅，(Ul ∪ Uh ) = ∅ の場合．

• イベントが発生した時，そのイベントに対応するタスクを優先度付きキューに追加する．

• 優先度付きキューの先頭にタスク τh が追加された時，まず，Jh のコピーフェーズで σ から得る Rh の

– 現在実行中のタスクの優先度が追加された状態と，Jl の実行後に Jh のコピーフェーズで σlタスク τh の優先度より低く，実行中のタスから得る Rh の状態は等しいため，(a) における

クと中断されているタスクの全てが τh に対

Jh の結果と (b) における Jh の結果が等しくな

してプリエンプティブルである場合，実行中る．また，Ul と Uh に共通部分がないため，一のタスクを中断し，タスク τh を実行する．

方のジョブの更新で他方のジョブの更新を上書き– それ以外の場合，現在実行中のタスクを継することがない．よって実行の結果をシステムの状態に書き戻す順番はシステムの最終的な状態に影響を与えない．よって σp = σlh となり，この場合も τl が τh に対しプリエンプティブルで
ある．

続する．

• 実行中のタスクが終了した時，優先度付きキューの先頭にタスク τh がある場合，– 実行を中断しているタスクがない場合はタスク τh を実行する．

(iii) τl で更新されるノードが τh で参照されず，τl– 実行を中断しているタスクがある場合，そと τh の両方で更新されるノードがある場合．

のうちのもっとも優先度が高いタスクを τi

2 と同様に，(b) における Jh の結果と (c) におとすると，∗ タスク τi が τh よりも優先度が低く，中に，より低優先度のタスクが実行を開始しており，そ断しているタスク全てが τh に対してプのタスクにプリエンプトできずに待機している時間でリエンプティブルである場合，タスク

ある．そしてもう一つは Self-pushing Phenomenon

τh の実行を開始する．

である．これは，対象とするタスクの実行によってよ∗ それ以外の場合，タスク τi の実行を再り高優先度のタスクの実行の開始が遅れ，それが最終開する．

的に対象とするタスクの実行を遅らせる現象である．

5. 4 スケジューラビリティ解析

解析は Level-i Active Period [6] という時間区間でスケジューラビリティ解析は，システムを構成する考える必要がある．Leval-i Active Period とは区間すべてのタスクがデッドラインを満たすかどうかを判[a, b) であり，t ∈ (a, b) となるすべての時刻 t におい

定するものである．つまり，タスクがリリースされたて優先度 Pi 以上のタスクで実行すべき状態にあるも時刻から実行が完了するまでの時刻の最悪の場合（最のが存在し，t = a と t = b において優先度 Pi 以上

悪応答時間）を考え，これがデッドラインを超えないのタスクで実行すべき状態にあるものがないようなかどうかを判定する．本節では，前節までで述べたス区間である．

このような現象があるため，スケジューラビリティ

ケジューリング方式におけるスケジューラビリティ解
析を行う．

ここまでで述べた概念を用いて，タスク τi の最悪応答時間 Ri を求める．

提案したスケジューリング方式は，特定の条件を満

まず Blocking Time Bi を求める．これは，τi よ

たす場合はプリエンプションを行い，それをを満たさり優先度の低く τi がプリエンプトできないタスクが，ない場合はプリエンプションを行わないというもので

τi のリリースの直前に実行を開始した場合を考えれある．そのため，PS と NP の中間的なスケジューリば良いので，

ング方式であると言える．そのような PS と NP の中

Bi = max{Cj − 1 | ∃h.(τh 6 ◁ τi ∧ Ph ≤ Pj < Pi )}．

間的なスケジューリング方式は，Limited Preemptive(1)

Scheduling として研究が行われている [8]．提案したLevel-i Active Period Li は，Bi に加え，Li のう

スケジューリング方式におけるスケジューラビリティ

ちにリリースされたすべてのタスクが完了するまで

解析は，この Limited Preemptive Scheduling のスの時間となる．よって

ケジューラビリティ解析の結果を参考に行う．
スケジューラビリティ解析は，最悪応答時間を求めることで行われる．最悪応答時間は，高い優先度のタ
スクの実行などによって対象としているタスクの実行がもっとも遅れるような状況を考えることで求められる．そのような状況を Critical Instant と呼ぶ．PSにおける Critical Instant は，対象となるタスクとそれよりも高い優先度のタスクすべてが同時にリリースされるような状況である．最悪応答時間の計算は，
この Critiacl Instant のもとで応答時間を求めることで行われる．
一方，低優先度のタスクが高優先度のタスクにプ
リエンプトされない場合がある時は他にも考慮すべ
き概念がある．そのうちの一つは Blocking Time である．これは，対象とするタスクがリリースされる前Li = B i +∑h.Ph ≥Pi

⌈

⌉
Li
Ch ．
Th

(2)

となる．よって，τi の最悪応答時間
Ri は，
⌈ ⌉
Li
Ki =
(3)
Ci
で表される Ki 個のジョブについて応答時間を求めれば良い．

k 番目のジョブの開始時刻 si,k は，Bi に加え，k − 1
個のジョブが完了するまでの時間と，si,k までにリリースされる τi より高優先度のタスクの実行時間を考慮することで求められる．よって，)∑ (⌊ si,k ⌋
si,k = Bi + (k − 1)Ci ++ 1 Ch ．
Thh.Ph >Pi(4)
k 番目のジョブの終了時刻 fi,k は，si,k に Ci を加え，さらに k 番目のジョブに対しプリエンプトして実行されるタスクの実行時間を考えれば良いので，Deferred Abort（DA）モデル [16] はそのうちの一つ

fi,k =si,k + Ci +∑で，タスクを二つの領域に分け，前半は AR モデル(⌈

h.Ph >Pi ∧τi ◁τh

fi,k
Th

⌉

(⌊
−

si,k
Th

⌋

))
+1

Ch

ングで実行するというものである．また，Deferred

(5)
となる．
最後に，k 番目のジョブの最悪応答時間はジョブの終了時刻からリリース時刻を引いたものとなるので，Ki 個のジョブについてそれらの最大値を取ることで，
Ri = max {fi,k − (k − 1)Ti }と求められる．

で実行し，後半はノンプリエンプティブスケジューリ(6)k∈[1,Ki ]よって，システムがスケジューリング可能であるための条件は，これまでで求めた最悪応答時間を用いて∀i = 1, . . . , n.Ri ≤ Di

(7)

となる．

Start（DS）モデル [18] も P-FRP の実行モデルの一つである．これは AR モデルにおける Non-work-

conserving なモデルで，タスクの実行開始時刻を遅らせて優先度の高いタスクの到着を待つことでプリ
エンプションの回数を減らしている．
本研究では，タスク同士の独立性に注目し，プリエ
ンプトされたタスクが再開時に最初からやり直す必
要がない場合にプリエンプションを行うことでタスクのやり直しをなくすスケジューリング方式を提案している．

PS でスケジューリング可能な場合は Self-pushing
Phenomenon が発生しない [17] ため最初のジョブのみ考えれば良いので，最悪応答時間の計算は

Ri =si,1 + Ci +∑h.Ph >Pi ∧τi ◁τh

(⌈

Ri
Th

⌉

(⌊
−

si,1
Th

⌋

Limited Preemptive Scheduling [8] は，プリエン
プティブスケジューリングとノンプリエンプティブスケ))+1

6. 3 Limited Preemptive Scheduling

ジューリングの中間的なスケジューリング方式である．

Ch

具体的なスケジューリング方式として，Preemption(8)

Thresholds Scheduling（PTS） [15]，Deferred Pre-と簡略化できる．

emption Scheduling（DPS） [3]，Fixed Preemption
Point（FPP） [7] の 3 つが提案されている．

6 関連研究本研究で提案したスケジューリング方式もプリエン

6. 1 同期的データフロー言語

プティブスケジューリングとノンプリエンプティブス

SIGNAL [4]，Lustre [11] は同期的プログラミング

ケジューリングを組み合わせたものであり，Limited

言語であり，リアクティブシステムの記述に用いられPreemptive Scheduling と類似している．一方で，提る．これらの言語では，クロックと呼ばれる値を明示案したスケジューリング方式は FRP が持つ制約を満的に扱うことで時間に関する記述を可能とする．

たすために設計されたものだが，Limited Preemptive

SCADE [9] は，Lustre や同じく同期的言語である

Scheduling はプリエンプションによるオーバーヘッ

Esterel [5] などを組み合わせて作られたプログラミ

ドを抑えるなどプリエンプティブスケジューリングよ

ング言語である．この言語はセーフティクリティカル

り効率的なスケジューリングを目指している，というな組込みシステム向けの言語であり，航空機や原子力点で相違する．

発電所などの制御システムの開発に用いられている．

7 結論と今後の課題
6. 2 P-FRP における実行モデル

本研究では，FRP によるリアルタイムシステムの

P-FRP では，前述の Abort-and-Restart（AR）モ

記述言語として，FreacTime では，個々のタスクとデルにおける優先度割り当てやスケジューラビリティ

そのデッドラインを明示的に記述することができる．

テストなど研究が行われている [19]．また，AR モデ

また，ノードに対しタイミングと呼ばれる抽象的な時

ル以外の実行モデルの提案もいくつか行われている．

刻情報を持たせることで，タスクにおいてどのノード

更新処理が行われるかを簡潔に表現することができる．さらに，ノードの関係をもとにしたタスク間の独立性を定義し，それを用いたスケジューリング方式を提案した．そして提案したスケジューリング方式に対するスケジューラビリティ解析を示した．
今後の課題としては，提案したスケジューリング
方式の評価が挙げられる．P-FRP では，Abort-and-Restart モデルが提案されており，その他の実行モデルに対するスケジューリング方式の提案も行われている．それらに対して本研究で提案したスケジューリ
ング方式との比較を行い，提案したスケジューリング
方式の有効性を調べる必要がある．また，FreacTimeの処理系の実装を行い，より実社会を意識したケース
スタディへの適用を行うことで，提案手法の有用性を示すことも今後の課題である．
謝辞 本研究の一部は JSPS 科研費 JP22K11967 お
よび JP24K14892 の助成を受けている．
参 考 文 献[ 1 ] Akesson, B., Nasri, M., Nelissen, G., Altmeyer,S., and Davis, R. I.: A comprehensive survey ofindustry practice in real-time systems, Real-Time
Systems, Vol. 58, No. 3(2022), pp. 358–398.
[ 2 ] Bainomugisha, E., Carreton, A. L., Van Cutsem,T., Mostinckx, S., and De Meuter, W.: A Survey on
Reactive Programming, ACM Computing Surveys,
Vol. 45, No. 4(2013), pp. 52:1–52:34.
[ 3 ] Baruah, S.: The limited-preemption uniprocessor scheduling of sporadic task systems, 17th
Euromicro Conference on Real-Time Systems(ECRTS’05), 2005, pp. 137–144.
[ 4 ] Benveniste, A., Le Guernic, P., and Jacquemot, C.: Synchronous programming with eventsand relations: the SIGNAL language and its semantics, Science of Computer Programming, Vol. 16,
No. 2(1991), pp. 103–149.
[ 5 ] Berry, G. and Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, Vol. 19, No. 2(1992), pp. 87–152.
[ 6 ] Bril, R. J., Lukkien, J. J., and Verhaegh, W. F.:
Worst-Case Response Time Analysis of Real-Time
Tasks under Fixed-Priority Scheduling with Deferred Preemption Revisited, 19th Euromicro Conference on Real-Time Systems (ECRTS’07), 2007,
pp. 269–279.
[ 7 ] Burns, A.: Preemptive Priority Based Scheduling: An Appropriate Engineering Approach, Advances in Real-Time Systems, (1994), pp. 225–248.

[ 8 ] Buttazzo, G. C., Bertogna, M., and Yao, G.:
Limited Preemptive Scheduling for Real-Time Systems. A Survey, IEEE Transactions on Industrial
Informatics, Vol. 9, No. 1(2013), pp. 3–15.
[ 9 ] Colaço, J.-L., Pagano, B., and Pouzet, M.:
SCADE 6: A formal language for embedded criticalsoftware development (invited paper), 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), 2017, pp. 1–11.
[10] Elliott, C. and Hudak, P.: Functional Reactive Animation, 2nd ACM SIGPLAN International
Conference on Functional Programming (ICFP
1997), ACM, 1997, pp. 263–273.
[11] Halbwachs, N., Caspi, P., Raymond, P., andPilaud, D.: The synchronous data ﬂow programming language LUSTRE, Proceedings of the IEEE,
Vol. 79, No. 9(1991), pp. 1305–1320.
[12] Kaiabachev, R., Taha, W., and Zhu, A.: E-FRP
with Priorities, 7th ACM/IEEE International Conference on Embedded Software (EMSOFT 2007),
2007, pp. 221–230.
[13] Sawada, K. and Watanabe, T.: Emfrp: A Functional Reactive Programming Language for SmallScale Embedded Systems, MODULARITY Companion 2016: Companion Proceedings of the 15th
International Conference on Modularity, ACM,
Mar. 2016, pp. 36–44.
[14] Sogo, K., Tsuji, Y., Moriguchi, S., and Watanabe, T.: Periodic and Aperiodic Task Description
Mechanisms in an FRP Language for Small-Scale
Embedded Systems, Proceedings of the 10th ACM
SIGPLAN International Workshop on Reactive andEvent-Based Languages and Systems, REBLS 2023,
New York, NY, USA, ACM, 2023, pp. 43–53.
[15] Wang, Y. and Saksena, M.: Scheduling ﬁxedpriority tasks with preemption threshold, Proceedings Sixth International Conference on Real-Time
Computing Systems and Applications. RTCSA’99(Cat. No.PR00306), 1999, pp. 328–335.
[16] Wong, H. and Burns, A.: Priority-Based Functional Reactive Programming (P-FRP) Using Deferred Abort, 2015 IEEE 21st International Conference on Embedded and Real-Time Computing Systems and Applications, 2015, pp. 227–236.
[17] Yao, G., Buttazzo, G., and Bertogna, M.: Feasibility Analysis under Fixed Priority Schedulingwith Fixed Preemption Points, 2010 IEEE 16th
International Conference on Embedded and RealTime Computing Systems and Applications, 2010,
pp. 71–80.
[18] Zou, X., Cheng, A. M. K., and Jiang, Y.: A
Non-Work-Conserving Model for P-FRP Fixed Priority Scheduling, 2016 13th International Conference on Embedded Software and Systems (ICESS),
2016, pp. 12–17.
[19] Zou, X., Cheng, A. M., and Jiang, Y.: PFRP task scheduling: A survey, 2016 1st CPSWeek
Workshop on Declarative Cyber-Physical Systems

(DCPS), IEEE, 2016, pp. 1–8.