【XDDP】変更要求仕様書をモデル検査、エクスモーションが検証アプローチを提案
エスクモーションの藤倉俊幸氏（コンサルティング本部 シニアコンサルタント）は、ソフトウエアの変更要求仕様書を基にして仕様内の矛盾や不整合などをモデル検査によって検出するアプローチを、2011年6月17日に開催された「XDDP（eXtreme Derivative Development Process）」のイベント「派生開発カンファレンス2011」において提案した。
変更要求仕様書に加えてユースケース記述を用意し、これらをLTSAやNuSMVなどのモデル検査器で形式検証するという流れである。車載分野のワイパー制御システムの仕様書に今回のアプローチを適用し、仕様上の未定義部分や矛盾、不整合を発見することに成功した。
XDDPは、組み込みソフトウエア開発に多い、派生開発や差分開発に特化した方法論で、システムクリエイツの清水吉男氏が提唱した。要求仕様における前の機種との差分を「変更要求仕様書」として、各変更要求がどのモジュールに影響するかを「変更要求トレーサビリティ・マトリクス」として、それぞれ記述する。デンソーなどがカーナビのソフトウエア開発にXDDPを活用している事例がある。
一手間掛けるだけで形式検証可能に
XDDPでは、「USDM（Universal Specification Describing Manner）」という手法で変更要求仕様を階層的に記述する。エクスモーションの藤倉氏は「階層構造が入っているということは、そこに包含関係などの論理構造が定義されているということ。通常のWordなどで記述された自然言語だけの要求仕様書と比べれば、セミ・フォーマルに近い記述になっている。USDMによる変更要求仕様書に一手間掛ければ、モデル検査器で形式検証できるようになる」と語った。
具体的には、変更要求仕様書の表の中に記述されている文章を単文に分解し、それらを「p1」「p2」といったように命題として定義する。その後、各命題間の論理関係をANDやOR、さらには「ならば（→）」などの論理演算子を用いて形式化する。必要な場合は、命題間の時間的な論理関係の変化も記述できる時相論理（temporal logic）も用いる。
ただし、XDDPは派生開発・差分開発に特化したアプローチであるため、記述の対象はあくまで変更・機能追加部分だけであり、既存部分については明示的にはモデル化がなされていない。変更・機能追加部分だけをモデル検査に掛けても仕様上の不整合などを検出しにくいため、今回はXDDPの変更要求仕様書に加えてシステム全体に関するユースケース記述も併用することで、この点をカバーした。
ユースケース記述のようなシステム全体の振る舞いはLTSAで、USDMによる詳細な変更要求仕様書はNuSMVで、それぞれチェックした。変更要求仕様書内にある表形式の仕様などは、NuSMV記述を手動で直接、書き下した。
仕様の不具合を5件検出
事例として、あるツール・ベンダーが開発したワイパー制御システムに、今回のアプローチを適用した。その結果、要求仕様間の矛盾、漏れなどを5件検出することができた。ユースケース記述内での未定義動作や仕様漏れが2件、ユースケース記述と変更要求仕様書の間での矛盾などが2件、変更要求仕様書内での不適切な仕様が1件、である。
【6/19開催NEアカデミー】
組み込みソフトはこうやってモデリングする
コード中心からモデル中心の開発へ
大規模・複雑化する組み込みソフトウエアを、どのように扱うべきか。その一つの答えが、ソフトウエアのモデリングです。現状の巨大なシステムがどのような構造を持っているのか。それを「設計図（モデル）」として適切に把握できなければ、次世代のソフトウエア・アーキテクチャは構築できません。本セミナーでは、静的構造図、動的構造図などソフトウエア設計図（モデル）の具体例を紹介し、「高凝集・疎結合」、「走り切り」といったソフトウエアの設計原則について解説します（詳細はこちら）。
