ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKOＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

概
組込みソフトウェア開発におけるイン-デザイン モデル検査

・イン-デザイン モデル検査の提案
ソフトウェア開発の設計工程で、仕様書のモデル検査を行う。
仕様書の不備、早期検出・修正を目指す。

−設計工程における仕様書のモデル検査の提案−

関西電力株式会社 電力技術研究所

篠崎 孝一

独立行政法人 産業技術総合研究所
システム検証研究ラボ

水口 大知

東光精機株式会社 ＮＷ機器開発部

石井 健志

2004/1/27

要・イン-デザイン モデル検査の試行
実際の組込みソフトウェア開発について試行した。
モデル検査の導入教育を実施した。
開発者とモデル検査技術者が協力して検査を実施した。
現実的な時間で、導入して検査結果が得られる
2004/1/27

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKOＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

１．イン-デザイン モデル検査

仕様書の問題点

発表の構成

問題点の見落とし個別の項目内は正しくても、別の項目と矛盾する

１．イン-デザイン モデル検査
２．ソフトウェア開発工程への適用
３．仕様書のモデル化

異常時 (*)処理が不十分(*)例

４．モデル検査の実施

・突然の停電、電源復帰
・操作手順誤り、ランダム操作・複数の操作を、同時に実施
・機械的な故障発生

５．実施結果・デッドロック（無限ループ）起こりうる問題 ・想定外動作の発生
・動作の不安定６．今後の取り組み

2004/1/27

2004/1/27

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

１．イン-デザイン モデル検査

過去の経験と異なる不具合は発見が困難

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

１．イン-デザイン モデル検査

仕様書のチェック

設計段階で、仕様書の内容をモデル検査することにより、問題点を解消して設計の品質を上げる。

システムの理解が不十分になりがち

仕様書（経験者の査読）（レビュー会議）

全ての可能性を考慮することは、不可能である。

2004/1/27

イン-デザイン モデル検査とは仕様書までの 手戻りをゼロにする。

モデル検査

手戻りが減少して開発期間が短縮する。

設計製作（コード化）
組込テスト

影響の大きな手戻りの発生を未然防止する。

販売・保 守2004/1/27

1ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

モデル検査の特質

１．イン-デザイン モデル検査

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

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

１．イン-デザイン モデル検査（仕様書）

網羅的な検査ができる・モデルと検査項目だけ記述すればよい・ツールが全ての状態遷移をつくして計算・テストパターンが必要ない

検査ツール
として強力

状態数が巨大なモデルは扱えない・メモリオーバーや計算の発散が起こる
・検査の精度とモデルの状態数の板ばさみ

検査項目検証したい内容を自然言語で明確化する。

機能１
機能１

状態遷移図の作成

機能１
機能１

時相論理式の作成
SPEC
E F(vend=COIN & pow = ON & can = OF
SPECAG(vend=COIN& pow = ON & can=OFF

仕様書の検査なら実用可能MODULE main
VAR
Home:boolean ;Bus:{on, off}
ASSIGNinit(PC) : = ON
next(PC):= case

検査プログラムの作成

検査結果のフィードバック

検査プログラムに時相論理式を追加（出力結果）
時相論理式１ true

仕様書のモデル検査は、ソフトウェア開発の効率化・品質向上に大きく寄与できる

時相論理式２ true
時相論理式３ true
時相論理式４false

検査ソフトによる自動検査

2004/1/27(falseの事例)

2004/1/27

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

２．ソフトウェア開発工程への適用

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

２．ソフトウェア開発工程への適用

本研究でのモデル検査体制

表１ モデル検査の教育

ソフトウェア開発者

モデル検査研究者

・開発システム ＯＫ・モデル検査？

・開発システム ？
・モデル検査 ＯＫ

協力体制

モデル検査の考え方

８時間

モデル検査言語（ＳＭＶ）

３０時間

モデル検査例題演習

５０時間

言語：ＳＭＶ，Ｓｐｉｎ，etc.
わかい ！ らなな使えい！

実際に開発中のプログラム 仕様書
2004/1/27

合計 ８８時間

next(a):={1,2,3}:
次は、1,2,3のどれか ？

？

2004/1/27

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

３．仕様書のモデル化

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

３．仕様書のモデル化

表２ モデル検査対象

2004/1/27？？
？

図３ モデル組み合わせの例

ＣＰＵ

８ｂｉｔ

実機の構成
ソフトウェアＯＳ

搭載せず

割り込み要因

８種類

記述言語

Ｃ言語

モデル検査対象

約６００行

ステップ数

約６００行
（全３５００行のうち）ハードウェア
外部入力

モデル構成
ソフトウェアモデル
ハードウェア
外部入力
モデル

仕様書のモデル化には、ノウハウが沢山あることが判明
2004/1/27

2

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKOＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

４．モデル検査の実施

発表の構成

表３ 使用した計算機環境

１．イン-デザイン モデル検査
２．ソフトウェア開発工程への適用
３．仕様書のモデル化

ＣＰＵ

３２ｂｉｔ

４．モデル検査の実施

動作周波数

３ＧＨｚ

メモリー

４ＧＢ

５．実施結果６．今後の取り組み

2004/1/27

2004/1/27

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

４．モデル検査の実施

項目

Ｃ言語のソースコード
ＳＭＶソース
コードの行数ハード部分

数ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

４．モデル検査の実施

表４ ソースコードに対するＳＭＶデータ

表５ モデル検査に要した時間
作業内容

量

項

仕様書のモデル化

約６００行
約７００行

モデルのコード化
ソフト部分

ＳＭＶでの状態数

目

時間

ハード部分

４

ソフト部分

２

ハード部分

２

約１２００行ソフト部分

４

約３０００万モデル検査（ＳＭＶの実行時間）

１３２

検査結果「false」の反例解析

１６
合計１６０時間2004/1/27

2004/1/27

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

４．モデル検査の実施

ＪａＳＳＴ ２００４
５．実施結果表６ 検出できた不備の要因
不備の要因

件数

開発者が想定していない変数に対する不正なアクセス

３

開発者が想定していない割り込みの発生

１

開発者が想定していない外部入力

１

割り込み処理のｵｰﾊﾞｰヘッド１

仕様書の記入不足

１

KEPCO／ AIST ／ TOKO

モデル検査の効果算定

モデル検査に要した時間

モデル検査の時間効果

８０時間
教育に要した時間

８８時間

１６０時間
完成後 のソフト改修と再テスト時間（推定 ８０時 間）が未然防止 できた。

現状では８０時間の損失

2004/1/27

2004/1/27

3

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

４．モデル検査の実施

ＪａＳＳＴ ２００４

KEPCO／ AIST ／ TOKO

４．モデル検査の実施

イン-デザイン モデル検査の実用性

表７ イン-デザイン モデル検査の課題現実的な時間で実施できた。

教える方も初めて教えた
実用ノウハウも集まっていない項

1.導入教育の効率化
８０時間の損失

最低限の効果算定方法

目説

明

専門書はあるが，実用面に重点を置いた教材がない．

2.モデル化の最初からノウハウを知っていれば，ノウハウ蓄積 もっと効率的に実施できた．
実用可能なレベルにある

3.検査手法の操作性向上

モデル検査器（ＳＭＶ）の操作性が悪い．

取り組みで判明した課題を改善して実用性能を、さらに改善できる
2004/1/27

2004/1/27

ＪａＳＳＴ ２００４
６．今後の取り組み

KEPCO／ AIST ／ TOKO

今後の取り組み・開発者向 けの教材開発
・モデル化ノウハウの習得と蓄積
・モデル検査器の操作性の改善
・検査を行う仕様書のレベル（上/下流）の指標検討
産業技術総合研究所システム 検証研究 ラボを中心に企業向けセミナーを準備中

2004/1/27

4