ソースコードの論理構造

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