Watchdogの設計-2 リセットのモデル

WDTの動作モデルを作ってみる。基本的な動作を並列合成することで目的の状態マシンを生成することが出来れば、要求仕様を組み合わせてそれを満たす状態マシンを作ることが出来る。そのサンプルとしてマルチタスク下のWDTの挙動を利用する。

動作の合成

定周期タスクの動作は左図で表される。これをLTSAモデルにすると

CTask = (body->alive->CTask).

となる。WDTはCTaskがbody部分で無限ループになるかデッドロックになってフラグにaliveを書き込まないとシステムリセットを掛ける。リセット動作は

ResetProcess = (Allaction->ResetProcess|reset->shutdown->END).

と書くことが出来る。ここでAllactionは、

set Allaction = {body, alive}

のように定義しておく。CTaskとResetProcessを並列合成する。

||CTaskWithReset = (CTask||ResetProcess).

このようにすると以下のような状態マシンが生成される。

興味があるのはreset時のタスクの振る舞いなのでCTaskWithResetからbodyとalive, resetだけの振る舞いを抽出する。

||CTaskWithReset = (CTask||ResetProcess) @{body, alive, reset}.

そしてミニマイズすると

リセットによって終了する動作が生成される。つまり、アプリケーションとしてのタスクの動きCTaskとシステム動作であるreset処理を別々にモデル化できると言うことである。
ResetProcessにAllactionとしてアプリケーション処理が入っているところがちょっとダサイがこれを入れないとresetで終了しない。CTaskが動き続けてしまう以下のような動作モデルが生成されてしまう。

参考文献

1) LTSA - Labelled Transition System Analyser