第4章

モデル検査ツールの利用

マルチコア環境におけるタスク設計検証

藤倉 俊幸

マルチタスク OS で動作するタスクは，割り込みなどの外的要因によってタスクの実行順序が変化し，それがバグの要因となることがある．タスクの実行順序を把握するためには，実行順序を全て洗い出し，ステート・マシンとして記述するという方法がある．従来は手動でこの作業を行っていたが，モデル検査ツール LTSA を使用することにより，ステート・マシンを自動出力できる．本稿では，形式検証を使ったマルチプロセッサ環境で動作するタスクの検証について解説する．
（編集部）

モデル検査ツールを使用したタスク設計の検証についてです．

は，CQ 出版社から刊行されている TECH I vol. 34「組みモデルと検査でモデル検査になるわけですが，要求や設込みソフトウェアの設計&検証」の 第 22 章以降で説明した計を対象とする場合には，要求分析を行う人や設計を行うことがあります．本稿は，その記事の内容を簡単におさら人が全ての可能な動きを把握できることには重要な意味がいし，マルチプロセッサ環境やマルチコア環境にどのようあります．つまり，検査なしでも有効な使い道があります．に適用するのかなどを，モデル検査にあまりなじみのない考えていることの全体を把握できることが重要なのです．

人でも分かるように説明したいと思います．

そこで，ここでは検査にはあまり立ち入らずに，まず「モデルとはどんなものか」，「全ての可能な動きとは何か」に1．モデル検査とはついて詳しく説明します．

● LTSA を使ってボールを取り出す問題を解く● 数学的な手法をソフトウェア開発に取り入れる形式手法（Formal Method）と呼ばれる手法があります．
この形式手法は，「数学を積極的に使ってソフトウェアを開発していこう！」という心意気に対して付けられた名前です．手法と言うよりはアプローチあるいは手法群と言った方が良いかもしれません．歴史は古く，コンピュータが非常に簡単なサンプルで考えてみましょう．高校などで習う順列組み合わせ問題です．
つぼの中に A というボールが 3 個と B というボールが 2 個入っているとする．ここから 3 個のボールを取り出すときの取り方は何通りあるのか？

使われ始めた頃から研究されていました．研究はされていこれは，順列組み合わせ問題の公式に当てはめれば，7ましたが，「難しすぎる」，「実際に使うにはコストが掛か通りであることが分かります．しかし，具体的にどのようりすぎる」などの理由から，ずっと日の目を見ない存在でな取り出し方が可能なのかは，公式を見ても分かりませした．しかし，この形式手法と呼ばれる一群の手法の中ん．これをモデル検査ツールである LTSA を使って解くに，「モデル検査」と呼ばれる分野があり，最近になって開と，具体的な 7 通りの動作パターンを作り出すことができ発現場で利用され始めています．

ます．

モデル検査では，検査対象になる要求仕様や設計仕様，

図 1 に，実際に LTSA のモデルと生成した動作パターン実際のコードなどから動きや操作に関する情報を抽出してを示します．動作パターンは，実際はつぼから A か B をモデルを作ります．このモデルは，全ての可能な動きのパ取り出す取り出し順で示すべきですが，ここではその取りターンを生成します．全ての可能な動きのパターンが生成出し順を生成するステート・マシンで示します．モデルとできたら，次に，一つ一つの動きを検査します．例えば，言っているのは，通常このステート・マシンのことです．

イベントの順番や特定のイベントが発生しているかなど

A= …，B= …と書いてあるのは LTSA に入力するソース・Nov. 2007

KEYWORD ―― 形式手法，モデル検査，RTOS，タスク設計，タスクの動作モデル，LTSA，ステート・マシン

81

Aが3個とBが2個の中から，合計3個を取り出す取り出し方は？
モデル
A＝（a->a->a->END）．
B＝（b->b->END）．
T＝（｛a, b｝->｛a, b｝->｛a, b｝->END）
．

3！
3！
3！
＋＋
＝7
3！
1！2！ 2！1！

aab0

1

2aaab34

56

789ab

図1
モデル検査ツールで組み合わせ問題を解く

abbbaab0bb2ba2bab2abab

図2
状態分析

abaa2a3abb
各状態は組み合わせに対応している

abaa

その状態に到達する経路の数が取り出し方の数1個取る 組み合わせは2通り a, ba2bb→b→a, b→a→b, a→b→b2個取る

組み合わせは4通り

2b, ab, ba, 2a2abb→a→a, a→b→a, b→a→a3個取る

組み合わせは3通り

a2b, 2ab, 3a3aa→a→a

コードに当たりますが，これをモデルと呼ぶこともありま

B，T はプロセス式と呼ばれています．これらを合成してす．それぞれ一つのモデルのテキスト表現とグラフィック一つにすることで，図 1 に示すようなステート・マシンがス表現だと思えば良いでしょう．

生成されます．このステート・マシンを分析することで，モデルの，A = (a->a->a->END).

いろいろなことが分かってきます．
LTSA が生成するステート・マシンの各状態は組み合わの意味は，「3 個ある A を一つ取り出す動作を a で表して，せに対応し，初期状態から各状態に到達する経路が具体的

それを 3 回行ったら終了する」，つまりなくなるという意

な取り出し動作列に対応します．図 2 に書き込んだコメン味です．

トのような，状態や経路の意味を日本語だけで記述するのB = (b->b->END).

は効率が悪く，正しく伝わるかどうか，そもそもまじめにも同じような意味です．これで，A と B だけをモデルにす読んでもらえるのかどうか怪しいものです．モデル化してると，合計 5 個あるボールを 5 個とも取り出す取り出し方あれば，グラフィカルに表現できるだけでなく，シミュを生成するモデルになります．ここでは，合計 3 個取り出レーションすることなども可能になります．こちらの方がす取り出し方が問われているので成果物としても優れています．

T = ({a,b}->{a,b}->{a,b}->END).

ステート・マシンから生成される動作列が「動作パターを制約としてモデルに追加します．{a,b}は「a か b を実行ン」となります．モデル検査ツールを使用すると，いろいする」という意味です．従って，T は a か b を実行するころなことが網羅的に分かるということが重要です．この性とを 3 回行うという意味になります．b は 3 回繰り返すこ質は，タスク設計だけでなくテスト・ケースの生成などにとはできないのですが，その条件は B に記述してあるのも応用できます．

で，T はこのままで良いのです．このようにして作った A，

82

つぼからボールを取り出す方法ではタスク設計との関連News Flash ――日立，人の動きや脈拍などのデータを 24 時間測定する腕時計型センサ・ネット端末を試作
日立製作所は，人の動きや脈拍などのデータを 24 時間測定する腕時計型センサ・ネット端末を試作した．3 軸加速度センサや脈波形センサ，温度センサ，マイコン，無線モジュール，電池などを内蔵する．毎秒 20 回の頻度で，10 日間連続して測定できる．

Nov. 2007