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

形式手法あれこれ

形式手法(Formal Method)と言われる分野にはおおざっぱに分けて形式仕様記述とモデル検査がある。それから、形式的開発手法というか開発プロセス的にまとめたものがある。

形式仕様記述ではVDM, Z等が有名である。モデル検査ではSPIN, NuSMV等が有名である。形式的開発手法にはB-method,RAISE等がありどれが有名と言うことはない。

VDMはツールの名前でもあるし言語の名前、あるいは記述スタイルを指して使われるが、Zは言語あるいは記法であり適当な専用ツールが無い。Zは好きだけど動かないからVDMを使う人は多い。それじゃZは使えないかと言うと事例はある。日本では使うの使わねぇのと言う段階から使えるのか使えないのかと言う議論が始まるまでに10年掛かったが、海外には成功事例も失敗事例もちゃんとある。

Zは集合論とλ計算など数学とコンピュータサイエンスの合わせ技で構成されている。形式的開発手法の中にも機能要求、非機能要求、動作要求を記述するためにCSP等のプロセス代数を組み合わせたものがある。組み合わせとしてはVDM/CSP/DC(Duration Calculus)が一番多いかも知れない。DCはインターバルロジックと言うこともある。

業務系だとVDMやZあるいは定理証明のCoq等が使われる。定理証明系のツールは難しいのでだんだん使われなくなっているとも聞く。例えばマスターカードなど。定理証明を使うよりモデル検査と組み合わせる方が楽かも知れない。

組込系だと動きの記述が重要になるのでプロセス代数系の手法が重要である。インターバルロジックも重要だがツールや適用事例をあまり聞かない。これからなのかも知れない。DCについては昔インタフェースに記事を書いたことがある。

組み込みソフトへの数理的アプローチ（第1回）時間仕様のあつかいガス・バーナー問題の例

USP友の会

業務系の話題だけれど、おもしろい人たちの存在を昨日知ってしまった。かなりの実績もあるという。RDBを使わずにシェルスクリプトだけで業務システムを構築する。開発費も運営費もIBMとか富士通がやる場合の1/10になるという。しかもパフォーマンスも良い。宇宙を飛ぶ怪しいムササビも良い。

データを書き足すだけで更新しない、検索しやすいようなファイルパスを設定する、書き込むデータ毎に別ファイルにする、ベースデータ以外は毎朝一から作り直すのでいつも新鮮(データの整合性が保たれる)、等々常識を覆すアイディア満載のシステム。既存のSIerは真っ青かも。

サブルーチン何か作らない。巨大なメインがあれば良い、その方が、早いから。
再利用なんかしない、似たプログラムを見つけてコピーして直して使う。クローンの何が悪いのさ
オブジェクト指向なんて要らない、インスタンスがあればいい。仕事をするのはインスタンスだ。

いつの間にかある種の価値観を刷り込まれていて、自分で納得も確認もしないまま従っていた様な気がする。

USP研究会ではなくUSP友の会、会社の名前はUSP研究所です。

ホームページの上の方にいるキャラクターは何ですか？

・「ちんじゅうちゃん」という名前のＵＳＰ友の会マスコットキャラクターです。むささびではありません。
・目から出ているのは、split光線といいます。この光線にあたったファイルは一瞬で数百万に分割されるそうです。
・将来的には、地球を守るために宇宙人と戦い、海のもくずと消える予定です。
・その数年後には、メカちんじゅうとしてよみがえることになっています。