2010/02/26

ソースコードの論理構造

要求を構造化した要求木と言う考え方を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

2010/02/23

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の評価