決定論的故障⇒決定論的原因故障

systematic failureを決定論的故障と呼ぶことにかなり違和感があった。ソフトにバグがあれば必ずおかしな動作をする。これが決定論的な動作で、そのような故障原因は安全ライフサイクルの様なシステマティックなアプローチで解決する。と言うことだと理解している。間違っていたら指摘してもらいたい。

日本語は原因の特徴について述べていて、英語は対処法について述べている。ここに違和感があったのだが、Webを見ていたら決定論的原因故障と訳している場合も多く、こちらであれば、「決定論的原因による故障」と解釈することで何とか納得できる。

決定論的原因とは原因箇所を論理的に絞り込めたり、それを証明することができるタイプの故障で、またそのことによって完全に取り除くことができる故障原因と定義してはどうだろうか。


例えばコンポーネントがA,B,Cとあってある機能Fが動かなくなってコンポーネン
トBをB1交換すると動く場合には、A, B, B1, Cがそれぞれ正常であるという命題とすると

￢(A∧B∧C)∧(A∧B1∧C)⇒￢B

によってBが原因であることを特定かつ証明できる。この論理式は常に真になる。取り替えてみてチャンと動けばOKと言う時の論理的根拠だ。しかし、

￢(A∧B∧C)∧(A∧B1∧C)⇒￢B1
￢(A∧B∧C)∧(A∧B1∧C)⇒￢A

では、偽になる部分があり見落としを指摘される。

ソフトの故障を確率的だ言う議論もあるが上記のような論法は成立するのでソフトの故障は決定論的だろう。キャッシュを使ったCPUにおけるソフトの実行時間は確率的と言っても良いが、それでも詳細に解析すれば場合の数が多いだけでその中のどれかに、条件を揃えることができれば確定する。条件を揃えると言うのはソフトウェアの外の話である。実際、おなじソフトをキャッシュ無しで動かせば確率的変動は取り除くことができる。で、これは取り替えてみてチャンと動くと言う論法で証明できる。

ソフトを含めたシステムで、そのシステムが正しく動いたとすれば、関連するモノ･コトの全てが正しいと言える。しかし、関連するモノ・コト全てを列挙することは不可能なので。検証可能なのは列挙できる要因だけになる。このことは、ある機能が正しいと言う命題をFとすると

F⇒A∧B∧C

と表現できる。前記の例をこの形式で書くと

(F⇒A∧B∧C)∧(F1⇒A∧B1∧C)∧￢F∧F1⇒￢B

となる。この場合、全ての場合でこの推論が成立するわけではなく、A, B, C, B1全てが正しい時が反例として検出される。すなわち、列挙できていない要因によってFが失敗した場合に対応する。ここで、FとF1はテスト結果と考えた方が良いかも知れない。

Cheddar: タイミング解析ツール

フリーのタイミング解析ツールCheddarを使ってみた。Windows版をダウンロードして解凍するとexeが出てくるのでそれをダブルクリックすれば立ち上がる。

一通り使えるだけの情報を提供するマニュアルもあるし、そこから関連する論文へのインデックスも付いているので時間を掛ければ色々面白いことができそうだ。
まず、プロセッサを定義する。Edit>Update Processorでスケジューラを指定する。RTOSの優先度ベースのスケジューリングに対応するのはHighest Priority Firstなので、これを選んでみる。この他にデッドラインモノトニックとか定番のモノが用意されている。Rate Monotonicを選べばタスク優先度を付けなくても良いので最初はこの方が良いかも知れない。独自に定義することもできる。

次にEdit>Update address spaceでメモリを定義する。取りあえず名前を付けるだけで先に進む。タスクとプロセッサとの対応付けはメモリによっておこなう様になっているのでメモリを定義しないとタスクの定義ができない。タスク定義はEdit>Update taskによっておこなう。適当な本に載っている例題を解いてみる。

以下の様にスケジュール可能であることが分かる。

これは使える。

implyとequivalent及びBranch coverageとDecision coverage

Twitterで話していたがまとめて話さないと伝わらないので、まとめてみる

ここに、Branch/Decision Testingという記事があって、冒頭に

For components with one entry point 100% Branch Coverage is equivalent to 100% Decision Coverage (入り口が一つのコンポーネントに対しては100%BCは100%DCと等しい)

と書いてある。

equivalentとは?
等しいのだからBDが100%ならDCも100%になりその逆も成立する。等価性には対称律が成立する。

入り口が複数あるとは?
構造化プログラム言語を使っていると関数の入り口は一つに決まっているが、昔のFortranのentry文を使うとサブルーチンの入り口を複数作ることができる。今でもOSのディスパッチャ等はマルチエントリの関数として実装されている。

この様な、プログラムでは100% Branch Coverage is equivalent to 100% Decision Coverageでは無くなる。

これとは別に


「デシジョンカバレッジとブランチカバレッジはお互いに、"A implies B"と定義されています。なので"A=B"となりますが、・・・」

と言うつぶやきがあり、これは違うでしょうと言ったのだけれど上の話と混ざってしまって140字では伝わらない。



implyとは?
implyとequivalentは違う。implyは片方向で、equivalentは両方向である。A implies B and B implies Aの時にequivalentと言って良い。これが対称律だ。

つまり

100%DC = 100%BC
DC⇒BC

は成立するが、

DC=BC

は成立しない。ここでBCと表しているのは、Branch/Decision Testingという記事で言えば

BC = {
B1 -> B2
B2 -> B3
B2 -> B9
B3 -> B4
B3 -> B5
B4 -> B8
B5 -> B6
B5 -> B7
B6 -> B8
B8 -> B2
}


と言う制御ブロック間の実行順序対の集合である。これは、元のプログラムのフローグラフの辺の集合として得ることができる。

一方、DCの方はプログラム内の論理判断の結果なので

DC = {

B2 -> B3

B2 -> B9

B3 -> B4

B3 -> B5

B5 -> B6

B5 -> B7

}

となる。従って

DC⇒BC

が成立していることが分かる。これは、DCの任意の要素を持ってくるとそれはBCの要素にもなっていると言う意味である。DCの要素ならばBCの要素でもある。これを省略して「DCならばBCである」と言うこともある。また

BC⇒DC

が成立していないことも分かる。これで、話は終わりかも知れないが、それなら100%DCだけど100%BCにならない例を見せてみろと尤もな突っ込みがあった。これは既に、シングルエントリの場合には、反例はないと言っているので、マルチエントリの場合を考えれば良いので、先のフローグラフの途中から実行を開始するようなパスを追加すれば良い。

だいたい
implyを暗黙に・・・等という訳の分からない日本語にするのが良くない。ことばを置き換えただけで分かったつもりになってしまう。

「ならば」と等価の区別はきっちり付けないといけない。アリバイがないから犯人にされてしまう世の中にはなって欲しくない。

カバレッジは幾つもあるが、そのカバレッジが定義する全体集合を実際に手で作って見れば色々なものが見えてくる。面倒くさいが実際に集合を作ってみて包含関係を見れば一目瞭然である。

Wot, no chickens?

Javaにはリアルタイム性が無いと言うと、ガベージコレクタの話題かと思うが、それだけではない。以下の二つも問題である。

1. Javaには待ち行列が二つある。Synchronizedによる待ち行列とwait/notifyによる待ち行列である。この二つの待ち行列のせいでライブロックが発生する。これはJava仕様の問題だろう。
2. それからもう一つ、待ち行列がFIFOではなくLIFOになっていることである。どこまでがJava仕様でどこからがVM実装依存なのか分からないが、現在ダウンロードできるJavaの実行環境はLIFOになっている。LIFOだと後から来たスレッドが先に処理されるので、オーバーロード時には最初に来たスレッドは永遠に待たされる。優先度付き待ち行列のポリシーはVM実装時に変更できないとどこかで読んだ気がするが、この記憶が正しければJava仕様の問題だろう。

これだけJavaが使われていて誰も問題にしないのは謎である。しかし、Androidがカーナビなどでも利用されるようになってくると問題になるのだろうと思う。

この問題を最初に指摘したのはKent大学のPete Welchで「wot, no chickens?」で検索すると今でも関連するページを見ることができる。サンプルコードも掲載されているので実験することができる。インタフェース誌にも小山尾 登氏の解説記事[1][2]が掲載されている。小山尾氏の実験によって現状のJavaVMの待ち行列がLIFOであることが分かった。IBMのサイト[3]でも説明されている。
Javaの問題点を指摘するためにBristol大学のAlan ChalmersがIEEE宛に1997年にレターを以下のメンバーと連名で送ったが無視されたらしい。レターの本文はしばらくWeb上にあったが今はアクセスできなくなっている。

Alastair Allen (University of Aberdeen, UK)
Andre Bakkers (University of Twente, Netherlands)
Richard Beton (Roke Manor Research Limited, UK)
Alan Burke (Aurigor Telecom Systems, Canada)
Alan Chalmers (University of Bristol, UK)
Barry Cook (University of Keele, UK)
Michael Goldsmith (Formal Systems (Europe) Ltd, UK)
Gerald Hilderink (University of Twente, Netherlands)
Ruth Ivimey-Cook (Advanced RISC Machines Ltd, UK)
Adrian Lawrence (University of Oxford, UK)
Jeremy Martin (University of Oxford, UK)
Nan Schaller (Rochester Institute of Technology, USA)
Dyke Stiles (Utah State University, USA)
Oyvind Teig (Autronica, Norway)
Paul Walker (4 Links, UK)
Peter Welch (University of Kent, UK)

それで、この問題を放置するわけにも行かないのでWelch達はCSPを使ってJavaの通信用ライブラリJCSP[4]を作成して公開している。使い方は、中原氏のホームページ[5]に解説がある。今後、組込でJavaを使うのであればJCSPを使った方が良いのではないかと思う。


[1] 並列プロセッサXMOSの検証環境PAT2
[2] UPPAALによる時間仕様検証
[3] JavaプログラマーのためのCSP　第1回
[4] Communicating Sequential Processes for JavaTM (JCSP)
[5] CSPモデルプログラミング

回文数式作成プログラム

プログラム検証ツールを使って回文数式を作る。
例えば

42+46=64+24


// 回文数式作成
void main()
{
  int a1, a2, b1, b2, A1, A2, B1, B2;
  __CPROVER_assume(a1 > 0 && a1 <10 && a2 > 0 && a2 < 10 && b1 > 0 && b1 < 10 && b2 > 0 && b2 < 10);
  A1 = 10*a1 + a2;
  A2 = 10*a2 + a1;
  B1 = 10*b1 + b2;
  B2 = 10*b2 + b1;

  assert((A1+B1) != (A2+B2));
}

このプログラムをCBMCに掛ければ検証に失敗して

State 7 file anagram.c line 9 function main thread 0

----------------------------------------------------

  anagram::main::1::A1=42 (00000000000000000000000000101010)

State 8 file anagram.c line 10 function main thread 0

----------------------------------------------------

  anagram::main::1::A2=24 (00000000000000000000000000011000)

State 9 file anagram.c line 11 function main thread 0

----------------------------------------------------

  anagram::main::1::B1=46 (00000000000000000000000000101110)

State 10 file anagram.c line 12 function main thread 0

----------------------------------------------------

  anagram::main::1::B2=64 (00000000000000000000000001000000)

State 11 file anagram.c line 14 function main thread 0

----------------------------------------------------

  c::main::$tmp::tmp$1=FALSE

Violated property:

  file anagram.c line 14 function main

  assertion (A1+B1) != (A2+B2)

  FALSE

VERIFICATION FAILED

を得ることができる。

7/1 追加
魔方陣の解き方
CBMCで魔方陣を作成するプログラムが公開されています。

単体テストできない関数

ヨーロッパの鉄道の安全規格[1]で一番厳しいSIL4ではブランチテストの100%カバレッジが求められるらしい。if文がネストしている複雑な関数の場合、そこにたどり着く入力データを作り出すのはなかなか難しい。CBMCを使って簡単にテストデータを生成する方法としてassert(0)を埋め込む方法がある。到達したい場所にassert(0)を仕込んで置いてCBMCで検証をすればCBMCが向きになってそこまで行って転けてくれるのでたどり着く方法が明確になる。必要があればprintf文も仕込んでおく、さらにテキストファイルに書き出すようにすれば、テストツールに掛けられる形でテストケースを得ることができる。

しかし、この方法も構造化されたプログラムでないとうまく行かない。構造化されたプログラムというのは、逐次、分岐、繰り返し構造だけでできているプログラムで、前方に跳ぶgoto文とか入れ子にならない繰り返しを持っていないプログラムである。今時、この様なプログラムはアセンブラで書かれたOSのディスパッチャぐらいだろう。ところが、並列性がある場合は任意のgoto文が動的に入るのと同じだからうまく行かない。要するに単体テストできないのと同じである。
グローバル変数を使っていても並列性が無ければ単体テストはできるが、それがvolatileなものだとそうはいかない。いちいちvolatile宣言しないとテスト以前にコンパイルがチャンとできているか心配になる。

並列性がある場合には、節操なくグローバル数を使うことは控えなければならない。空海がどのように並列に文章を書くのか、文章だけはできていて出力だけが並列なのか、文章も考えながらつじつまの合うものを書き出すのか、これはアーキテクチャがぶれていては実現できない。
グローバル変数を多用して、並列性のあるシステムを作っていて、単体テストもチャンとやってますとか言う組織は多いけれどどんな単体テストをやっているのだろうか。

[1] European Committee forElectrotechnical Standardization. Railway Applications -
Communication, signalling and processing systems - Software forrailway control
and protection systems, http://www.cenelec.eu

PDD その2

インタフェース誌にPDDのアイディアを書いた[1]。基本的な手順は、

1.      プログラムの目的を事後条件として表す。assert文で表現する。

2.      入力条件を場合分けし、それを事前条件とする。assume文で表現する。

3.      assume文の範囲でコーディングをおこない、検証をパスさせる。

4.      パスさせる過程で反例を分析して、分析結果はコーディングまたは事前条件に反映させる。

5.      残りの入力条件について同様に検証をパスさせる。

6.      全ての入力条件に対して検証が終わったら、事前条件を整理する。

基本的にはプログラムSを下のような形にして、Q∧Ｓ⇒Rを満たす様にする。QとRがプログラムの仕様である。入力条件は実装後はテスト条件として使用できる。

assume(Q);
S;
assert(R);

似たような形をコンピュータのセキュリティ改善に使っている論文があった[2]。この論文ではダイクストラの最弱事前条件を使っている。プログラム検証ツールを使用すれば自動化できる部分もありそうだ。

何もしないスキッププログラムの場合は、S=TrueなのでQ⇒Rになる。プログラム検証ツールは含意論理式の証明器としても使えることが分かったので、[1]ではちょっとした実験を紹介した。この実験を発展させて仕様書検証に使えないか検討してみた。すなわち、VDMで言うところの、陰関数定義をCで書いて検証できれば、仕様検証になる。やってみたら、確かにできそうだが、C言語で事前条件・事後条件を書くのが結構大変である。おかげで、述語論理を使えるVDMや時相論理を使えるモデル検査ツールの便利さが分かった。
モデル検査ツールはテストケースを用意しなくても検証できるが、述語論理式はテストケースが必要になる。と言うことはPDDの過程で作成するテスト条件が述語論理式をC言語で記述するヒントになるのかも知れない。
自然言語から直接Cの様なプログラム言語を書き出すのと、一端、述語論理式を経由するのでは、後者の方が絶対に楽なはずだ。壁の正体は何だろうか?

[1]新・組み込みソフトへの数理的アプローチ（第12回）
テストとプログラム検証――TDD（テスト駆動開発）におけるテスト

[2]B. V. Chess. Improving Computer Security using Extended Static Checking. In Proc of. 2002 IEEE Symposium on Security and Privacy, pages 160-173, 2002.

レビューの信頼性

レビューする時、間違っているのに正しいとしてしまう間違いと、正しいのに間違っているとしてしまう間違いの二通りの間違いがある。前者をtype-1、後者をtype-2の間違いとする。またそれぞれの発生確率をe1、e2とする。要するにtype-1は見落とし、type-2は濡れ衣を着せてしまうことに対応する。

一人で2回レビューする時、1回目で間違いとしたものは見直さない場合には、見落としの確率は低くなるが、濡れ衣の確率は高くなる。xをe1またはe2としてプロットすると上図のようになる。つまり、見落としの方は二回連続で見落とさない限り検出されるので、見落とし確率はe1*e1になる。0 < e1 < 1なので小さくなりレビューの信頼性は向上する。濡れ衣は一度着せられてしまうと脱げないので、着せられてしまう確率は高くなるのである。濡れ衣を着せられない確率は1-e2で二回連続で着せられない確率は(1-e2)*(1-e2)になる。従って、一度でも着せられてしまう確率は1-(1-e2)*(1-e2)になる。これが上図の濡れ衣確率である。レビューしている本人にはどっちの間違いを犯したか判断は付かないというか、そもそも気づかないから間違いなのでどうしようもない。

逆に、一回目のことはすっかり忘れたことにして二回目のレビューをして両方で検出されたもののみを間違いとする場合は、今度は見落とし確率が高くなる。二人で1回レビューする場合で、二人が一致したもののも間違いとする場合も同様である。どちらかが間違いとしたものを間違いとする場合には、再び濡れ衣確率が高くなる。要するに必ずどちらかの間違い確率が高くなってしまう。

そこで、二人で二回レビューすることにすると、間違いのタイプによって挙動が変わる。見落とし型の間違いは以下のようになる。一回の間違い確率が0.38より大きいと信頼性が下がる。

濡れ衣型の間違いは以下のようになり、一回の間違い確率が0.61以上だと信頼性が下がる。

いずれにしても、おっちょこちょいな人が混じっているとレビューの信頼性は悪化する。と言うかやらない方が良いかも。

TDD ⇒ PDD

ダイクストラは、テストでバグの存在は示せるがバグのないことは示せないと言っていた。一方で、TDDはテストを重ねながらプログラミングをおこない、用意したテストが全部通ったらプログラム完成と言うアプローチだ。と誤解しやすいが実は単なる開発プロセスに対する提案である(10/2)。
欲しいのはバグはあるかも知れないが取りあえず動作する綺麗なコードではなく、まずバグのないコードだ。
この点を改善するにはどうするか。実は良いアイディアが浮かんだ。自動テストツールではなく、プログラム検証ツールを使用して正しいことを証明しながらプログラミングをおこなうPDD(Proof driven development)だ。
プログラムSの証明とは、Qを事前条件、Rを事後条件として、{Q} S {P}が恒真であることを示すことだ。たとえば、二つの整数x, yを与えられてxが大きい値になるように、値を入れ替えるプログラムを書きたいとする。つまり


main()
{
  int x, y;

  assert(x >= y);
}

と言うことだ。これは関数仕様になる。Qは無しつまりQ = { T }、R = { x >= y }である。このソースコードをプログラム検証ツールのCBMCに掛けると当然

Violated property:

  file proof0.c line 8 function main

  assertion x >= y

  FALSE

VERIFICATION FAILED

となり正しくないことが証明される。次にもともとxの方が大きい場合をQに設定して検証する。つまり以下のプログラムを検証する。ここで、__CPROVER_assume( );はCBMCで前提条件を設定するディレクティブである。

main()

{

  int x, y, tmp;

  __CPROVER_assume( x>=y ); // Q1

  assert(x >= y);

}

これは成功する。従って x >= y の時は何もしなくて良いことが証明された。次にこのQが否定された場合を考える。￢(x >= y) だから(x < y)だ。

main()

{

  int x, y;

  // __CPROVER_assume( x>=y ); // Q1

  __CPROVER_assume( x < y ); // Q2 = ￢Q1

  if (x < y) {

  }

  assert(x >= y);

}

これは失敗するのでif文の中を書いて


main()
{
  int x, y, tmp;

  if (x < y) {
    tmp = x;
    x = y;
    y = tmp;
  }
  assert(x >= y);
}

とすると

>cbmc proof0.c

file proof0.c: Parsing

proof0.c

Converting

Type-checking proof0

Generating GOTO Program

Function Pointer Removal

Starting Bounded Model Checking

size of program expression: 18 assignments

simple slicing removed 1 assignments

Generated 1 VCC(s), 1 remaining after simplification

Passing problem to propositional reduction

Running propositional reduction

Solving with MiniSAT2 without simplifier

761 variables, 2109 clauses

SAT checker: negated claim is UNSATISFIABLE, i.e., holds

Runtime decision procedure: 0.034s

VERIFICATION SUCCESSFUL

となって正しいことが証明された。(x >= y)∨(x < y)は恒真なのでQ= {T }となり仕様が満たされた。

ダイクストラの時代にはプログラム検証器が無かったので手で証明しなければならず実用にはならなかったが、今は検証器がある。現在この手法の体系化を進めている。プログラミングが終わった時に、使い古しのテストケースとバグがあるかも知れないコードを得るTDDよりはPDDの方が良いことは言うまでもない。しかもdivision by zeroの様な普通のテストではできない検証も可能である。

モデル化のセンス

Use Caseモデルを作ろうとするとDFDのような数珠つなぎの絵を描いてしまう、なぜだろうか、と聞かれたのでしばらく考えていた。たまたまUML&FMと言う形式手法関係のIEEEのワークショップの資料を見ていたところ下図のような絵があった。

きっとMulti-viewのところの知識か何かが不足しているのでそのようなことになるのではないか。例えば、DFDの使い方には長けているので何でも本人は書けてしまうし良く理解できている。何でもExcelで書いてしまう人などこのタイプは多い。自分用のメモとしては良いかも知れないが、他の人には理解してもらえない。変てこな図を書いていても作るものは作っているのであれば、抽象化軸やアーキテクチャ軸は頭の中に存在しているのだろう。Multi-view軸のところには色々なタイやグラムが並んでいるが目的に応じて使い分けることをUMLは意図している。下の図のような状況をUMLはある程度回避できるが、意味的な厳密さが無いので十分ではないと言うのがUML&FMでは話題になっている。

アーキテクチャとViewと言えばKruchtenの4+1 Viewが有名だ。

上記の図はオリジナルの論文[1]に掲載されているものでRational Softwareの資料では多少変更されている。

RUPにおけるそれぞれのビューの説明は以下のようになっている。

ユース ケース ビュー: アーキテクチャ上重要な振る舞い、クラス、技術面でのリスクを含むユース ケースとシナリオが含まれます。ユース ケース モデルのサブセットです。

論理ビュー: 最も重要な設計クラスとそのクラスからパッケージとサブシステムへの編成、これらのパッケージとサブシステムからレイヤへの編成が含まれます。ユース ケースの実現も含まれます。設計モデルのサブセットです。

実装ビュー: 実装モデルと、モジュールの観点からのパッケージとレイヤへの編成の概要が含まれます。実装ビューのパッケージとモジュールへの、(論理ビューの) パッケージとクラスの割り当ても記述されます。実装モデルのサブセットです。上の図ではコンポーネントビューと表示されている。

プロセス ビュー: 関与するタスク (プロセスとスレッド)、そのタスクの相互作用と構成、タスクへの設計オブジェクトとクラスの割り当ての記述が含まれます。このビューは、システムにかなりの程度の並行性がある場合にのみ使用する必要があります。RUP では、設計モデルのサブセットです。

配置ビュー: ほとんどの典型的なプラットフォーム構成のさまざまな物理ノード、物理ノードへの (プロセス ビューの) タスクの割り当ての記述が含まれます。このビューは、システムが分散される場合にのみ使用する必要があります。配置モデルのサブセットです。

それぞれのビューに向いたダイヤグラムがあるのでそれを使い分ければ良いモデルになるだろう。と言えれば美しいが、実際はUMLに存在するほとんどのダイヤグラムは論理ビュー向きである。動的な表現のために、シーケンス図とか状態図があるがタスク構造を表現するには不十分で、プロセスビューを記述することはできない。それでヨーロッパではADLが作られた。タスク構造を表現するための図としては、Gommaの図などがUML以前からあったが今は忘れられている。その意味ではプロセスビューが重要になる組込システムをUMLでモデリングしろ言われてもできないのが当然で、論理ビューの記述だけして実装に入ってしまう人の方がむしろ疑問が残る。

4+1ViewではユースケースビューからプロセスViewを構築することになっているが、ユースケースモデルで描くシーケンス図等の動的仕様とタスク設計の間にはまだギャップがある。どちらかというとユースケースモデルよりもプロブレムフレーム[3]による要求分析の方が動的な要求を正確に獲得できる気がする。ちなみに[4]は親子で書いた論文でプロブレムフレームとAlloyをどう融合するのかと言う面白い論文である。
プロブレムフレーム⇒Concurrency⇒Gomaaの流れが動的なモデリング、つまり動的アーキテクチャ構築には必要だと思う。ここでConcurrency[5]はLTASの教科書である。

参考文献

[1] Philippe Kruchten 著 1995, "The 4+1 view model of architecture," IEEE Software. 12(6), November 1995.

[2] Hassan Gomaa, Software Design Methods for Concurrent and Real-Time Systems.

[3] Problem Frames: Analysing and Structuring Software Development Problems (Addison-Wesley, 2001)

[4] Daniel Jackson and Michael Jackson,Separating Concerns in Requirements Analysis: An Example.

[5] Concurrency: State Models and Java Programs

ソースコードの論理構造

要求を構造化した要求木と言う考え方を2010年2月号のインタフェース誌で紹介した。

要求管理ツールなどで要求のトレーサビリティを管理する例はあるが、それは単なる関係ではなくて論理的関係である。このことを利用して知識ベース化しようと言う考え方である。
今月のインタフェース誌(2010年4月号)はこの続きで、要求木の一番下のソースコードとの関係をプログラム検証ツールCBMC ( Bounded Model Checking for ANSI-C )を利用してソースコードも論理式にしてしまって要求木に組み込んで見ようと言う試みである。

上の図でCが左のソースコードの論理式表現になる。Rがアサーションでソースコードが満たすべき仕様になる。要求木の図ではReq6とかReq7にあたる。
CBMCはソースコードを論理化するのが目的ではなくPolySpaceと同じようなソースコード検証をするためのツールである。PolySpaceに比べるとフリーのツールなので使いづらいが、同じソースコードに対して同じ箇所の問題を指摘してくれる。ただし、PolySpaceと違って指摘の仕方がちょっと分かりづらい。また、Bounded Model Checkingを使っているので無限ループになることを検出するのは無理だ。

参考文献
[1] A Tool for Checking ANSI-C Programs,
http://www.kroening.com/papers/tacas2004.pdf
[2] astah 6.1 で「要求モデル」が目指している姿 T

Simics

エリクソンの基地局ソフトのデバッグのために開発されたシミュレーション用のツールSimicsを、ウィンドリバーのセミナーで見てきた。シミックスと読むらしい。

http://www.co-nss.co.jp/products/middleware/simics.html

バーチャテック・ジャパンと言うところが日本法人らしいがまだ日本語のホームページがない。英語のページに行くとホワイトペーパーがそろっている。ゾウムシのような虫の写真付きのホワイトペーパーがあった。スエーデンの虫だろうか?

ボードレベルのシミュレーションを行うことができる。システムLSIのシミュレーション等でサイクルアキュレートだと数ミリ秒分の実行で一晩かかったりするが、このツールはボードを仮想化してハードウェア部分のメモリとかバスのシミュレーションはやらないのでサクサクと動く。Windowsの時計のシミュレーションのデモを見たが実時間より早く動く。面白いのはログを取っておいて逆実行ができる。また、ハードが故障した状態を設定することもできる。通信で特定のデータだけ遅延やロストしたときどうなるかについて実験することもできる。
Windows上でLinux動かすデモでは、2コアのうち一つのコアのクロックを遅くしたときの実験とか、止めてしまったときの実験をしていた。
シミュレーションするためのハードのモデル化にどの程度手間がかかるのか分からないが、これがあればタスク設計の善し悪しの判定が楽になる。DML(Device Modeling Language)というC言語を拡張した言語でハードをモデル化する。eclipseベースのモデリング環境がある。このモデルがハードのスペックになるのでハード屋さんが作ってくれると更に楽だ。
Linuxのシミュレーションが出来る評価ライセンスがあるらしい。

6/7 追加: Virtutech（Simics等の製品ですね）はWindriverに買収されたそうです。

参考文献
[1]システムシミュレータSimicsを用いたLinux Super Pageの評価

原因結果グラフ-2 MASK

結果グラフで　A masks B とした場合の扱いは

1) A⇒￢B
2) Aが真ならBは未定義(三値論理の利用)
3) Aの真偽による場合分け

の三通りが考えられる。

1)の場合REQ制約の否定として表現できる。CEGTestの場合は、問い合わせ中だが、REQの否定を柔軟に利用できればMASKは要らなくなってしまう。 赤い四角で囲った部分を表現することが出来るので1)の意味でのMASKは特に必要ない。

青丸で囲んだところはちょっと怪しい。と言うか括弧で括るような、否定を取る優先順位を決めなければならない。そう言うことを考えなくても良いようにREQとMASKが定義してあると言うのは合理的かも知れない。ただし、最近FXの秋山氏の指摘で新たな謎が生まれた。MASKは結果側に付ける[1]と言うものである。もしそうなら原因結果グラフは結構簡単で使いやすいものになる気がする。この謎の裏にどんな合理性があるのか調べてみたい。


2)調べてみると三値論理には何種類もある[2]。マスクされた側をどう解釈するか(a.真か偽か決まらない状態、b.真でも偽でもない第三の状態、c.無意味)によって使用する論理系が変わる。VDMはaによって未定義を扱える。ただし、実装上の都合で一部変更して利用している[3]。用途によって結構自由に使って良い見たいな感じである。原因結果グラフを命題論理の範囲で扱うことを考えているので、各ノードは命題でなければならず、単に真偽が決まっていない状態とするのが話が難しくならなくて良いと思う。VDMの様な手直しをするかどうかはまた別の問題として考えれば良いだろう。三値論理を使うと、結果側に不定が現れる。結果側に現れる不定が妥当かどうか、ちゃんと解釈できるかどうかで使用する論理系を決めれば良いと思う。それで、幾つかやってみたが三値論理を使わなかった場合すなわち、1)の方法で真にも偽にもなり得るという結果に落ち着く。aの場合の真理表は以下のようになる。*が真偽が決まらない状態。赤いところをVDMでは*として扱う。

A	B	A∧B	A∨B	A⇒B	￢A
T	T	T	T	T	F
T	F	F	T	F
T	*	*	T	*
F	T	F	T	T	T
F	F	F	F	T
F	*	F	*	T
*	T	*	T	T	*
*	F	F	*	*
*	*	*	*	*

3)“A masks B”をAが真の時はBを考慮しなくて良いというそのままの意味に解釈して。Aが真の時はBを含まない原因結果グラフを作ってしまう。これは、原因結果グラフ全体を表す論理式の真偽がどのような意味を持つのかに関わる問題と関係する。


参考文献
[1] http://en.wikipedia.org/wiki/Cause-effect_graph
[2]http://ja.wikipedia.org/wiki/3値論理

原因結果グラフを利用した形式仕様記述

形式仕様記述というと述語論理から始まるが、命題論理でもやれることは多い。その一つが原因結果グラフである。これについては以前インタフェース誌[1]に書いたことがある。しかし、最近ニフィのK氏がCEGTestをリリースされたのだがどうも仕様が違う様なので悩んでいる。また、FXのA氏のツール(X-CEG)とも違う様だ。特にMASKの扱いが違う。それで本当はどうなのか少し整理しておきたい。インタフェース誌[1]に掲載した変換規則を以下に示す。元ネタは[2]である。EとOは要素数が3ヶ以上の時は論理式の形が変わる。それは[1]を参照。

原因結果グラフの本来の使い方はテストケースを絞り込むことであり、仕様を記述することではない。仕様記述としてはMC/DC等の手法を使って絞り込む前の論理式表現に興味がある。同じ文章から原因結果グラフを作っても人によって違うグラフが出来ることが多い。それは元の文章の解釈の違いを反映するが、論理式で表現すると論理的には等価であることが分かったりする。等価でなくても、どこが違うか明確化できて仕様の解釈のブレをなくすことが出来る。

取りあえず以下の3点が気になっている。

(1)まず原因から結果に向かう線の解釈だけれど、私は⇒(ならば)でなく⇔(同値)をディフォルトで使用していた。これは問題文に依存して決めるべき。例えば、料金表などでは同値関係にしないと別の条件でも同一料金になることを認めることになる。排他的に扱いたいかどうかで使い分ける必要があるだろう。

切符の払い戻しの場合、誤購入の時は必ず払い戻すのであれば
(誤購入)⇒(払い戻し)
となる。払い戻すのは電車が止まってしまった時にも行われるので
(払い戻し)⇒(誤購入)
は成立しない。と言うようなことを考察しないと決められないのだと思う。
一般的には、原因結果グラフの元になる文章はある特定の状況を表すフレーズなのでその範囲では、電車が止まってしまうことなどは想定しない場合が多いので
(誤購入)⇔(払い戻し)

として良い場合が多いように思う。つまり普通は、
(誤購入)⇒(払い戻し)　または　(誤購入)⇔(払い戻し)
だろう。逆向きになるのは原因が目的で、結果が実現方法の様な場合かも知れない。
別の見方としてこれは論理関係ではなく定義であると思った方が良い場合もある。結果を定義しているdefine文のようなものであり、結論を一つの素命題とするのではなく単なるラベルと考える。

(2)MASKは三値論理を使用するのが正しいかも知れない。しかし、その場合結果も不定になることがある。結果が不定でも良いのかは元の文章を書いた人に確認する必要がある。たぶん不定は意図していないのではないか。

(3)これが一番重要かも知れないけれど、原因結果グラフの論理式が真になると言うことがその仕様が矛盾無いと言うことを表す。形式仕様記述は全体が真になる範囲で分析をする。偽になるところは、あり得ないと元の文章を書いた人が言っているところだから分析の対象外にする。テストの場合は、全体の真偽はあまり考えないのか? 全体が偽になるところから選んだテストケースはハードが故障した場合とかユーザーのオペレーションミスのテストに対応するのか?


幾つか事例についてそれぞれのツールの結果を比較してみたい。長くなったので(2)と(3)はまた改めて。


参考文献
[1] 新・組み込みソフトへの数理的アプローチ（第6回）

原因結果グラフ――原因と結果の関係を木構造で表現する

[2]

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光線といいます。この光線にあたったファイルは一瞬で数百万に分割されるそうです。
・将来的には、地球を守るために宇宙人と戦い、海のもくずと消える予定です。
・その数年後には、メカちんじゅうとしてよみがえることになっています。 

信頼性について-2: MTTFによるテスト

クリーンルーム手法では品質保証を目的としたテストの指標としてMTTF(Mean Time To Failure)を利用する。そして、バグ密度のような指標は品質にとっては意味がないと言っている。クリーンルーム手法はホーア理論に基づいた形式手法の一種である。

また一方、ソースコード検証ツールであるPolySpaceのWebセミナーは

1. プログラム検証によって発見されたソースコードのバグを100%取る必要は無い。95%ぐらいでよい。
2. 機能テストとプログラム検証は違う。
3. プログラム検証をやっても機能テストは必要だ。5%の取り残しバグがあっても機能テストをパスすれば良い。

と言っている。

クリーンルームの方は、機能テストをすればプログラム検証は必要ないという言い方になっていて一見すると別のようだが、障害の有無が重要でありfaultの数は重要でないと言う点では一致している気がする。バグは欠陥(fault)に対応し障害(failure)と同じでないことはすでに述べた。テストの世界では、ホワイトボックステストとブラックボックステストという分類があるが、ホワイトボックスはfaultの検出、ブラックボックスはfailureの検出と対応づけることができるかも知れない。

クリーンルームでは、ユーザの使用特性を分析して、それに基づいて実際にシステムを動かしてMTTFを測定する。ある欠陥が発見されてから次の欠陥が発見されるまでの時間がMTTFになる。このMTTFがある値以上になれば出荷基準に達したと判断する。

クリーンルーム手法によってプログラムを作ればfaultは無いはずだからfailureの検出が重要だとも説明している。またfaultの無いプログラムを高品質と定義している。faultの無いプログラムであればMTTFの測定が出来る。それでどのようなテストをするかというと、品質を測定するためのテストであり、まず利用モデルと言うものを作る。利用モデルには以下のものが含まれる。

利用者: システム外部の実態、アクターやデバイスなど
利用の仕方: 動作モデル
環境: プラットフォーム、利用の状況(昼/夜、緊急時、オートモード)

動作モデルは、状態遷移図や決定表で表現される。利用モデルからテストケースを生成するには利用の仕方の統計的情報が必要になる。具体的には各遷移の遷移確率を入れた状態マシンを利用する。同値分割とかは利用しない。ソースコードの作り方はシステムの品質とは無関係と考える。具体的にどのようにテストケースを生成するのか、MTTFをどのように測定するのかについては色々な論文を読まなくてはならない様だ。

参考文献

信頼性について

品質と同じようにわかり辛いのが信頼性だ。ソフトにバグが有ると品質も信頼性も低くなることは依存はないと思うが、バグが無ければ高品質で高信頼性かというとそうでもない。仮にそうだとしてもバグの無いソフトはない、あるいはバグの無いことを証明することはできないとも言われるので、ソフトについて高品質とか高信頼性とか言うと嘘つきになって、話が終わってしまう。そんな訳だからあまり人と議論してもまともな議論にならないことが多い。もっと定量的な定義が必要である。
品質属性の一つとして信頼性があるというのが一般的なので、信頼性から考えてみたい。障害が起きるかどうかは確率的事象と考えることが妥当である。f(t)を障害が起きる確率密度関数とすると。ある時刻tまでに障害が起きる確率分布関数F(t)は以下のようになる。

障害を広辞苑で引くと「2. 身体器官に何らかのさわりがあって機能を果さないこと」と出ている。この何かのさわりがソフトではバグと言うことになる。ソフトウェアにバグ(fault, 故障)があると処理結果に誤り(error)が生じる。処理結果が間違っているとそれはシステムの障害(failure)になる。誤りがあっても必ず障害が発生するとは限らない。たとえば、リレー接点が焼き付いてしまって常時ONになった場合でも、OFFにしようとしない限り障害として顕在化することはない。ソフトウェアにバグがあれば必ずエラーは起こるが、障害というレベルで考えると確率事象であると言う主張は、言われてみればそんな気もする。

それで、障害が発生しない確率を信頼度(reliability)と定義する、と言ってもどんな状況でシステムを動かしてなのかがはっきりしないと意味が分からない。電源を入れた瞬間火を噴かない確率なのか、ある機能を利用しようとしてちゃんと使える確率なのかが分からない。そこで、火を噴くとか、機能しない等は故障としてまとめてしまう、そうすると電源を入れた瞬間か、機能を使おうとした時かと言うことが残る。これは、障害がいつ起こるかと言うことだから、信頼度は電源を入れた時からt時間までに障害が発生しない確率と言う意味と考えれば良い。すると信頼度は時間の関数なのでR(t)と表せば、F(t) = 1 - R(t)である。

障害が起きる確率と信頼度の関係が見えてきた。f(t)が何かがもう少し分かるとスッキリする。ある時刻tまで順調で、時刻tとt+dtの間に障害が起きる確率をλ(t)とすると、f(t)はR(t)とλ(t)の掛け算になる。λを障害率(failure rate)と呼ぶ。このλを時間に対して定数とするとR(t)は以下のようになる。

ソフトには時間による劣化のようなことは無いのでλが定数と言うのは妥当な気がする。だからλが分かればソフトウェアシステムの信頼性が定義できるかも知れない。ソフトのバグは踏めば必ず爆発する地雷のようなものだから、システム障害が発生する確率はどんな歩き方をするかに依存する。全ての歩き方を考慮すればランダムな歩き方と言うことになり指数分布になるのは納得がいく。ハードの場合には、初期故障がありしばらくすると落ち着いてまた摩耗が起こると障害率が上がるバスタブ型になるが、ソフトの場合はそのようなことはないので上記の信頼度の関数はハードよりもソフトに当てはまる。

障害までの平均時間(Mean Time To Failure: 平均寿命)と言う尺度がある。これは以下のように表せる。

そしてこれを実際に計算すると何と

となるのである。完成したシステムのフィールドでの平均障害発生時間を調べればソフトウェアの障害率がわかる。後は、バグの数あるいはバグ密度と障害率の関係が分かれば面白くなる。

Prism

テクマトリクスでのPrismの説明会に参加した。Prismは、プログラムの動的解析をするツールである。
入力としては、デバッグ情報付きのオブジェクトコード、実際に実行して得たトレース情報、ソースコードである。
　マルチタスクやマルチコア環境でのチューニングやシングルコアからマルチコアに移行する際の設計支援に利用することが出来る。ソースコードを入力として利用するのでソースコードを解析するのかと思っていたら、解析対象は実行トレースであった。別々のスレッドが同じアドレスにアクセスしていたらソースコードを参照してアラートを上げてくれる仕組みである。従って、実行した部分のみが解析対象になる。排他制御が必要なのに排他制御されてないと、タイミング上実際に不具合が無くても不具合の可能性として検出する。また、アドレスを見ているので、ポインターのポインターのそのまたポインターによる参照でも検出することが出来る。ソースコード解析ではなかなか難しいが直接アドレスを見ているので簡単に検出できるわけである。また、ヒープの中でも解析できる、メモリーリークの検出ばかりでなく、freeするタイミングを早くすると次のmalloc待ちのスレッドが早く動けると言うようなメモリーの使い回しのチューニングをシミュレートしながら出来る。なかなか良い機能だ。
　静的解析でデータ依存が報告されるがパフォーマンスのボトルネックになるものがどれかを予測することは難しいが、what-if解析でどの依存を解消すべきかについてもシミュレーションで優先度を決めることが出来る。
　製品の目的はシングルコアからマルチコアに移行する際の設計支援だが、シングルコア/マルチタスク環境におけるタスク設計のチューニングにも応用できる。30日の評価版があるので実際に使ってみようと思う。


2010.08.29: 書き足し
確率モデル検査をおこなうPRISMとは違う

マルチタスク環境におけるWatchdogの設計

Watchdogタイマーは基本的にはカウンターでzeroになった時かオーバーフローした時にシステムにリセットを掛けてシステムを再スタートさせるハードウェア部品だ。組込屋さんは、PCプログラマのことをバグがあってもリセットすれば良いと思ってる見たいに偉そうに言うが、実はWatchdogはそれを自動化したものだ。やばい時にはリセットするのは変わりない。
ここでは、どんな使い方をするのかまとめてみる。組込では、RTOSを使う場合と使わない場合があるが面白いのはRTOSを使った場合である。以降はWatchdogタイマーをWDTで表す。

要件(やりたいこと)

1. OSやタスクの無限ループ、デッドロックの検出をする
2. 低優先度のタスクが動けることのチェックをする
3. 単に動くだけではなく、アプリケーションに応じて健全性チェックをする

設計(つくりかた)
WDTをkickするタスクをモニタータスク(MTask)とする。その他のタスクをアプリケーションタスクとする。アプリケーションタスクを定周期タスク(Cyclic Task, CTask)とイベント駆動タスク(Eventdriven Task, ETask)に分類する。

イベントドリブンタスク
定周期タスクには有効そうだが、イベントドリブンタスクに対してWDTはどんな効果があるのか? と言うか要件は実現可能か?　外部イベントはいつ来るか分からない、来ないかも知れない。だから、イベント待ちの状態はWDTのモニタ対象外にする。その状態をasleep状態とする。

Sanity Flag
各アプリケーションタスクにフラグを持たせる。alive, asleep, unknownを値として持つ。このフラグはatomicに読み書きできるようにintかcharにする。と言うかCPUのレジスタサイズにする。CTaskとETaskは書き込みのみ、MTaskは読み書きする。MTaskが書き込むのはunknownのみ。CTaskが書き込むのはaliveのみ。

動作
健全性チェックは各アプリケーションタスクがおこなう。CTaskは問題がなければフラグにaliveを書き込む。ETaskはイベント待ち状態に入る際に問題がなければasleepを書き込む。待ちが解除されたらaliveを書き込む。
MTaskは起床されたら、各フラグをcheckしてaliveかasleepだったらWDTをkickしする。aliveフラグをunknownに書き換える。WDTをkickしなければシステムはリセットされる。参考文献-1のFig.3は定周期タスクとモニタタスクの動きを示している。ただし、アプリケーションタスクをシステムタスクと呼んでいる。



参考文献
1) Watchdog Timers