ソフトウェアテストシンポジウム 2004
JaSST’04: Japan Symposium on Software Testing 2004

組込みソフトウェア開発のイン-デザイン モデル検査−設計工程における仕様書のモデル検査の提案−
篠崎 孝一†

水口 大知††

石井健志††††関西電力株式会社電力技術研究所〒661-0974 兵庫県尼崎市若王子 3-11-20
独立行政法人産業技術総合研究所システム検証研究ラボ 〒661-0974 兵庫県尼崎市若王子 3-11-46†††
東光精機株式会社ＮＷ機器開発部〒566-8686 大阪府摂津市千里丘 3-14-40††

E-mail: †K576789@kepco.co.jp, ††daichi.mizuguchi@aist.go.jp, †††TAKESHI_ISHII@toko-s.co.jp
あらましソフトウェア開発の設計工程において仕様書のモデル検査を行う「イン-デザイン モデル検査」を提案する．これにより，仕様書の不備の早期検出・修正を目指す．さらに，このイン-デザイン
モデル検査を，実際の組込みソフトウェア開発に対して試行し，その効果，問題点，および実現性について検討した結果を報告する．
キーワード モデル検査，ソフトウェア開発，設計，組込み，仕様書

In-Design Model Checking for Embedded Software−A Proposal of Model Checking for Specification in Design process−
Koichi SHINOZAKI†

Daichi MIZUGUCHI††

andTakeshi ISHII††††Power Engineering R&D Center, Kansai Electric Power Company 3-11-20 Nakoji, Amagasaki-shi, Hyogo, 661-0974 Japan††

Laboratory for Verification and Semantics, National Institute of Advanced Industrial Science and Technology
3-11-46 Nakoji, Amagasaki-shi, Hyogo, 661-0974 Japan†††Distribution Network Equipment Development Department, TOKO SEIKI CO.,LTD3-14-40 Senrioka, Settsu, Osaka, 566-8686 Japan

E-mail:†K576789@kepco.co.jp,††daichi.mizuguchi@aist.go.jp, †††TAKESHI_ISHII@toko-s.co.jp

Abstract We propose the In-Design Model Checking which incorporates model checking of specifications into thedesign process of software development, aiming at the early detection and correction of specification errors.
We report on our trial application of the In-Design Model Checking to an actual embedded softwaredevelopment with the examination of its effectiveness, problems and feasibility.
Keyword Model Checking，Software Development，Design，Embedded，Specification

1. は じ め に
高度情報化社会の進展に伴い，大小さまざまなシス
テムソフトウェアが生活に密着して稼働しており，そラミングよりも前に検出して修正することができれば，ソフトウェアの信頼性向上と開発作業の効率化に大きな効果が期待できる．の信頼性確保は必要不可欠な問題である．また，ソフ

本研究では，仕様書に対してモデル検査を適用する

トウェア開発者の立場からは，ソフトウェアのテスことで，システムに起こりうる全ての状態を網羅的にト・修正に費やされる莫大な作業時間が，開発コスト検査し，仕様書の不備の早期検出・修正を行う手法を削減の障害となっている．

「 イ ン -デ ザ イ ン モ デ ル 検 査 」 と し て 提 案 す る ．

テスト工程でバグが発見された場合には，前工程にさ ら に ， こ の イ ン -デ ザ イ ン モ デ ル 検 査 を ， 実 際 の戻って原因究明を行い，修正作業を行う．特に発見さ組込みソフトウェア開発に対して適用する体制を整えれたバグが仕様書に起因する場合には，ソフトウェアて試行し，その効果，問題点，および実現性についての設計工程に戻って修正を行う必要がある．これにか検討した結果を報告する．

かる労力は大きく，また新たなバグを生み出す可能性がある．
よって，仕様書に潜在している論理の矛盾や設計者にとって予想外の動作といったバグの原因を，プログ

2. イ ン -デ ザ イ ン モ デ ル 検 査
ソフトウェア開発は，顧客の要求仕様書から始まり，システム仕様書から機能仕様書，プログラム仕様書と目指す．
イ ン -デ ザ イ ン モ デ ル 検 査 の 作 業 の 流 れ を ， モ デ ル

要求分析

検 査 器 Ｓ Ｍ Ｖ （ Symbolic Model Verifier） (3) を 使 っ た 場
仕様書
仕様書

合 を 例 に と っ て 説 明 す る（ 図 ２ ）．ま ず ，仕 様 書 を 状 態

設計

遷 移 図 と し て モ デ ル 化 し (a)，こ れ を モ デ ル 化 言 語 に よﾌﾟﾛｸﾞﾗﾐﾝｸﾞり 記 述 し て Ｓ Ｍ Ｖ コ ー ド を 作 成 す る (b)．さ ら に 仕 様 書

モデル検査組込テスト

もしくは，事前の知識に基づいて検査項目を抽出・設販売・保守

定 (c)し て ， そ れ ら を Ｃ Ｔ Ｌ (Computation Tree Logic)と
呼 ば れ る 時 相 論 理 式 に よ っ て 記 述 す る (d)．次 に ，こ れ

図１

イ ン -デ ザ イ ン モ デ ル 検 査らを入力としてモデル検査器を実行する．モデル検査器は，入力したモデルが検査項目を満足するかどうか段階を追って機能が細分化されて行く．しかし，こを 自 動 的 に 計 算 し て 結 果 を 回 答 す る (e)．

れらの仕様書には，論理の矛盾や作成者にとって予想外の動作といったバグの原因が潜在している．

モ デ ル が 検 査 項 目 を 満 足 す る 場 合 に は 「 true」 が ，満 足 し な い 場 合 に は 「 false」 と 反 例 （ 検 査 項 目 を 満 足

こうした仕様書の不備を取り除くために，査読が行し な い 状 態 遷 移 の 例 ）が 出 力 さ れ る ．「 false」が 回 答 さ

われるが，査読者の技能と経験に依存するため十分なれた場合には，反例を解析することによりその原因を実施が難しく，手戻りの原因となっている．

究 明 す る (f)．モ デ ル 化 の 誤 り や 時 相 論 理 式 の 誤 り が 原

そ こ で ， イ ン -デ ザ イ ン モ デ ル 検 査 で は ， 仕 様 を 細因の場合には，それらを修正して再度，モデル検査を分化して設計を行う工程の中で，仕様書に対してモデ行う．そうでない場合には，仕様書そのものの不備が

ル 検 査 を 導 入 す る （ 図 １ ）．

原因と考えられるので，その修正を行う．これらの作モデル検査とは，状態遷移系として記述されたシステムが，時相論理式で表された検査項目を満足するかどうかを数理的に判定する手法である(1)

業 を ，「 false」が 回 答 さ れ な く な る ま で 繰 り 返 す こ と で ，仕様書に潜在する不備を手直しする．

．モデル検査では，システムの全動作を網羅的に検査することがで

3. ソ フ ト ウ ェ ア 開 発 工 程 へ の 適 用きるので，査読に比べて厳密な検査が可能である．
今日では，モデル検査を計算機上で自動的に実行す(2)

研究者によるソフトウェア仕様書のモデル検査は，
こ れ ま で に も 発 表 さ れ て い る (4)(5) ．今 回 は ，イ ン -デ ザ

．イ ン -イン モデル検査を実際のソフトウェア開発工程に対デ ザ イ ン モ デ ル 検 査 で は ，モ デ ル 検 査 器 を 用 い た 自 動して適用する試みとして，ソフトウェア開発者がモデ的なモデル検査を，設計段階において仕様書に適用すル検査の教育を受けた上で研究者と協力してモデル検る．これにより，仕様書の不備の早期検出・修正を査を行なう体制を整えた．

る ツ ー ル（ モ デ ル 検 査 器 ）が 公 開 さ れ て い るa.モデル化

b.コード化
機能１
機能１
機能１
モデル

実現したい
システム
（顧客の要求）

仕様書
仕様書
仕様書
設計書
仕様書
設計書
設計書
設計書

e.検査
ＳＭＶコードモデル検査器MODULE
MAIN （モデルの記述）

PC

VAR
・‥‥‥‥‥

出力結果

状態遷移図

c.検査内容抽出

ＣＴＬ

検査内容

SPEC

項目２ true

項目１…
項目２…
項目３…
項目４…

（検証内容記述）

項目３ true

論理式１

項目４ false

日本語で記述‥‥‥‥‥d.ＣＴＬ作成

仕様書手直し図２

項目１ true

イ ン -デ ザ イ ン モ デ ル 検 査 の 流 れ

f.解析

実機の構成表１ モデル検査の教育内容
モデル検査の考え方
8 時間
モデル検査言語（ＳＭＶ）
30 時 間モデル検査例題演習

モデル構成

ソフトウェア
ソフトウェアモデル

50 時 間ハードウェア

開発者は，モデル検査について全くの初心者からスタートして，表１の教育を受講してから，ある組込みソフトウェアの仕様書のモデル検査を行った．モデル

外部入力

ハードウェア
外部入力
モデル

検査の経験がある研究者は，開発者から仕様書の説明を受けてソフトウェアの動作を理解しながら，開発者

図３

モデル組み合わせの例と協力してモデル検査を実施した．
インデザインモデル検査を試行したソフトウェアを実施した．この様子を図３に示す．の概要を表２に示す．対象とした組込み機器は，新規開発品であり，ソフトウェアおよびハードウェアの併

5. モ デ ル 検 査 の 実 施

行開発のため，設計時点ではハードウェアが存在して今回の試行では，モデル検査器として前述のＳＭＶいなかった．また，仕様書全部ではなく，一部の機能を用いた．ＳＭＶは状態遷移系の内部表現に効率的なに つ い て の み 検 査 を 行 っ た ．設 計 後 の C 言 語 に よ る プ

データ構造を用いており，比較的多くの状態数を扱う

ロ グ ラ ミ ン グ の 結 果 ，全 体 で お よ そ 3500 行 の シ ス テ ム

ことができる．ＳＭＶを実行した計算機環境を表３にと な っ た が ， そ の う ち お よ そ 600 行 に 相 当 す る 部 分 を示す．

検査対象とした．
今回は，モデル検査とは別に，従来どおりのソフトウェア開発も併行して行っており，モデル検査の結果を適時，従来設計に反映する流れとした．

表３ 使用した計算機環境
32 bitＣＰＵ3 GHz
動作周波数4 GB
メモリーモデルから作成したＳＭＶコードの行数と状態数

4. 仕 様 書 の モ デ ル 化
一般に，上流の仕様書にはシステムの持つ機能が比較的大きな単位で記述されており，下流側の仕様書でを 表 ４ に 示 す ．Ｃ 言 語 と Ｓ Ｍ Ｖ の コ ー ド 行 数 の 違 い は ，文法の違いによるものである．

は機能が細分化され，プログラム言語に沿った形で処モデル検査に必要な検査項目は，プログラム製作仕理が記述されている．今回は，開発者のニーズに基づ様書に記述されたシステムの動作，上位の仕様書に記

き，プログラムに近いレベルでの詳細な仕様の不備を載されている動作，明示的に示されていない分野固有検出するため，最も下流側のプログラム製作仕様書をの知識等に基づいて，開発者が作成した．また，ハー検査対象としてモデル化した．

ドウェア及び外部入力部分のモデルが期待通りに作成

今回使用したプログラム製作仕様書は，フローチャされていることを確かめるための検査項目も別途作成

ートを主体に記述された仕様書であった．開発者は，し た ．そ の 結 果 ，検 査 項 目 は ，合 わ せ て 99 個 と な っ た ．

検査を行いたい箇所を抽出しモデル化を行った．

こうして作成した検査項目をＣＴＬにより記述し，順

また，今回モデル化を行ったソフトウェアの中には，ハードウェアの割り込みにより起動する部分があった
ため，ハードウェアのモデル化も併せて行った．
さらに，ハードウェアの中には，外部からの入力を必要とするものがあったため，外部入力部分のモデル化も行った．これら３つのモデルを組み合わせて検査次，検査モデル（ＳＭＶコード）に追加してモデル検査器で検査した．
今 回 ， 全 検 査 項 目 に つ い て 図 ２ に 示 し た a.モ デ ル 化
か ら f.解 析 ま で の 繰 り 返 し に 要 し た 時 間 は ， 約 160 時間であった．作業時間の内訳を表５に示す．
表５の時間には，モデル化，コード化の誤りやＣＴＬ論理式の誤りを含んだ状態でＳＭＶを実行して結果表２ モデル検査対象
8bit
ＣＰＵＯＳ
搭載せず割り込み要因
8 種類
記述言語
Ｃ言語
モデル検査対象
ステップ数

約 600 行(約 3500 行 の う ち )表 ４ ソ ー ス コ ー ド に 対 す る SMV デ ー タ
項目
数 量
Ｃ言語のソースコード
約 600 行
ＳＭＶソース
ハード部分
約 700 行
コードの行数
ソフト部分
約 1200 行
ＳＭＶでの状態数
約 3000 万表５ モデル検査に要した時間
作業内容
項 目
仕様書のモデル化
ハード部分
ソフト部分
モデルのコード化
ハード部分
ソフト部分
モ デ ル 検 査 （ SMV の 実 行 時 間 ）検 査 結 果 「 false」 の 反 例 解 析

時間422413216

表 ７ イ ン -デ ザ イ ン モ デ ル 検 査 の 課 題
項目説明
1.導 入 教 育 の専 門 書 は あ る が ，実 用 面 に 重 点 を 置効率化
いた教材がない．
2.モ デ ル 化 の最初からノウハウを知っていれば，ノウハウ蓄積 もっと効率的に実施できた．
3.検 査 手 法 のモ デ ル 検 査 器（ Ｓ Ｍ Ｖ ）の 操 作 性 が操作性向上
悪い．

を解析した時間も含まれている．ＳＭＶの実行１回て現実的な作業時間で実施でき，成果が得られるこに要した時間は，数秒から数時間の範囲で大きくばらとが確認できた．対象ソフトウェアに高信頼度を要求

つ い て い る ． Ｓ Ｍ Ｖ の 実 行 に よ り 「 false」 が 得 ら れ た

される場合、新規開発で知見が不足する場合には，十場合の反例解析を，開発者と研究者が協力して実施し分な効果が期待できるものと考える．て す る こ と で ，過 去 の 例(５ )と比較して効率良く解析作

今 回 の 取 り 組 み 結 果 を 踏 ま え ，さ ら に イ ン -デ ザ イ ン
モデル検査の作業時間を短縮するための課題について，業を進めることができた．
全ての検査により，7 件の仕様書の不備が検出できた．そのうち，システムの動作として実際に支障とな作業を行った開発者と研究者の意見を元に取りまとめた結果を表７に示す．

る も の が 3 件 ，支 障 を 発 生 し な い も の が 4 件 で あ っ た ．

7. 今 後 の 取 り 組 み

検出できた不備の要因を表６に示す．
システムをプログラム製作仕様書のレベルでモデ

イ ン -デ ザ イ ン モ デ ル 検 査 を ソ フ ト ウ ェ ア 開 発 手 法

ル化していることから，ハードウェアに依存したソフと し て 確 立 す る た め に ，以 下 の 取 り 組 み を 進 め て い く ．

トウェアの詳細な動作に関わる不備を検出できている．

・開発者向けの教材開発を行い，効率よく習得するための機会を設ける．
・様 々 な ソ フ ト ウ ェ ア 仕 様 書 を 対 象 に イ ン -デ ザ イ ン

6. 実 施 結 果
今 回 の 事 例 を 基 に ， イ ン -デ ザ イ ン モ デ ル 検 査 の 費
用 対 効 果 を 検 討 す る ．教 育 に 要 し た 88 時 間 を 除 き ，イモデル検査を行ない，モデル化のためのノウハウを 得 る と 共 に ，こ れ を 再 利 用 で き る 形 で 蓄 積 す る ．

ン -デ ザ イ ン モ デ ル 検 査 の 実 施 に 160 時 間 を 要 し て 7・モデル検査器の操作性を改善する検討を行う．

件の仕様書の不備を検出したことを効果として算定す・検査を行う仕様書のレベル（上流／下流）についる に は ，様 々 な 方 法 が 考 え ら れ る ．今 回 は ，イ ン -デ ザて適切な指標を検討する．

イ ン モ デ ル 検 査 の 実 施 に よ っ て ，テ ス ト 工 程 後 の ソ フ

なお，教育に関しては，既に産業技術総合研究所のトウェア改修および再テストに要する時間（改修内容

システム検証研究ラボを中心として一般企業向けセミ

か ら 経 験 で 80 時 間 と 見 積 り ）が 発 生 し な か っ た ，と 考ナーの準備を進めている．

え て 推 定 効 果 の 最 小 値 を 80 時 間 と す る ．
推 定 効 果 80 時 間 か ら イ ン -デ ザ イ ン モ デ ル 検 査 の実 施 時 間 160 時 間 と 差 し 引 き す る と ，80 時 間 の 損 失 である．初めて実際の製品開発にモデル検査を導入する
今回の事例では，実際に開発作業を効率化するには至っていない．しかし今回，理論研究やツールの進歩にもかかわらず，これまでは実用化に遠いと思われていたモデル検査が，実際の開発現場において教育も含め
表６検出できた不備の要因
不備の要因
開発者が想定していない変数に対する不正なアクセス
開発者が想定していない割り込みの発生
開発者が想定していない外部入力
割込み処理のオーバーヘッド
仕様書の記入不足

件数
311
11文

献

[1] E. M. Clarke, O. Grumberg, and D. A. Peled: ModelChecking, The MIT Press, 1999.
[2] B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A.
Petit, L. Petrucci, Ph. Schnoebelen, and P. Mckenzie:Systems and Software Verification; Model-Checking
Techneques and Tools, Springer, 2001.
[3] A. Cimatti, E. M. Clarke, E. Giunchiglia, F.
Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani
and A. Tacchella,
NuSMV 2: An OpenSource Tool
for Symbolic Model Checking,Proceeding ofInternational
ConferenceonComputer-AidedVerification (CAV 2002), pp. 27-31, Copenhagen,Denmark, July, 2002.
[4] 寺 田 博 文 ， 土 屋 達 弘 ， 菊 野 享 ， 記 号 モ デ ル 検 査を用いたステートチャートの検証 ，信学技報，
SS98-41， pp17-24， Jan.1999.
[5] 早 水 公 二 ， 篠 崎 孝 一 ， 高 橋 孝 一 ， 渡 邊 宏 ， モ デル検査器を用いた自動検針システムの仕様検証 ，
産業技術総合研究所算譜科学グループ研究速報，
AIST-PS-2003-005, June, 2003.