簡易な形式仕様記述と状態遷移表を併用した要求仕様書のレビュー方法
水口大知（独立行政法人産業技術総合研究所）
漆原憲博（株式会社ジェーエフピー）

１．概要
要求仕様書に潜む論理的欠陥を効率的に指摘するための方法論を提案する。事例として、SESSAME による「話題沸騰ポット要求仕様書第 7 版」に適用したところ、100 件以上の指摘事項が抽出できた。これは提案手法の有効性を示すものである。
キーワード：要求仕様書、レビュー、形式仕様記述、状態遷移表

２．背景
高信頼または安全なシステムの開発には、要求仕様書の完成度を十分高めておく必要がある。しかしながら現実には、要求仕様書の欠陥に起因して多くのシステム不具合が発生し、また、大きな手戻り作業が生じていると言われている。これらを防ぐことを目的として、欠陥を生みにくい要求仕様書の記述方法と、欠陥を抽出しやすいレビュー方法を提案する。

３．課題
システム開発においては、設計工程では準形式手法および形式手法の導入が進んでいるのに比べて、要求仕様書は自然言語で記述されることが一般的である。そのため、曖昧な記述や記述のゆれが発生しやす
く、不具合や後工程からの手戻りを誘発している。これらを排除できるような記述およびレビューの方法が必要である。
記述の曖昧さをなくすための技術としては、形式仕様記述言語があり、VDM や Z 言語、B メソッドなどが知られている。これらを適用したシステム開発事例も報告されているが、一般的な方法論としては浸透していない。その原因としては、形式仕様記述言語が、数学や論理学の記法を用いていることから記述や読解が難しく、スキルが求められることがある。ましてやこれを、システム発注側と受注側との合意形成の手段として用いることは現実的でない。
以上の状況を打開すべく、要求仕様書の可読性を維持しつつ記述の厳密性を確保するために、適度な形式性を備えた記法を開発して、形式的記述をサポートするためのツールを開発した。さらにツールを活用した要求仕様書のレビュー方法を開発した。

1/6

４．内容
提案する要求仕様書のレビュー手順は以下の①～④の段階からなる（図 1）。
① 要求事項を SLP で記述する② SLP で状態遷移表を作成する③ 状態遷移表を眺めて、おかしなところを見つける④ 要求事項および SLP 記述を修正する（①へ）。

図 1 要求仕様書のレビュー手順①から④の手順について、例を交えて以下に説明する。

①

要求仕様記述には、株式会社ジェーエフピーが開発したツール（SPEC L-PERFECT; SLP）を使用する。ツールの画面イメージを図 2 に示す。
SLP では基本的に、Do 文と if 文の組合せによって要求事項を記述する。記述例を表 1 に示す（話題沸騰ポット要求仕様書第 7 版からの例）。ここで、if 文は条件分岐であり、Do 文は命令文である。

if 文および Do 文において、<・>の中身をメンバー名と呼び、{・}の中身を状態名と呼ぶ。

図 2 SLP の画面イメージ

2/6

表 1 SLP による要求事項の記述例

要求番号pot-330-41
アイドル中に蓋センサ on となったら、沸騰行為に遷移する。

原文

if <ポットの状態>{アイドル中}
if <蓋センサ>{on}Do<ポットの状態>{沸騰行為にせよ}
else
next

SLP 記述

endif
else
next
endif
指摘・修正事項②

・原文では、「アイドル」、「沸騰行為」の主語が明記されていないので、「ポットの状態」を明記する。

Do 文にかかる if 節の条件をメンバー名毎に集めることにより、メンバー名毎の「状態遷移表」を得ることができる。SLP は、この状態遷移表を自動作成する機能を持っている。例えば、話題沸騰ポット要求仕様書のメンバー名「ポットの状態」については、表 2 のような状態遷移表が得られる。

表 2 「ポットの状態」の状態遷移表（一部）
蓋●ポットの状態

水量

沸騰ボタン

ポットの状態

ブザー

蓋センサ

全ての水

※３位センサプラグ※２
沸騰行為にせよ 閉じられた 適正－－－－－－－－－

100msec 以 保温行為中∧~ [100msec
沸騰行為にせよ －－上押された沸騰行為にせよ －－※１ －保温行為にせよ －－－

給湯中

鳴らせ]

アイドル中－－on－－－－－－－－off

カルキ抜き加熱を終えた
コンセントにアイドルにせよ －－－－－
つながれた(保温行為中)∨
アイドルにせよ －－－－－(沸騰行為中)
・・・

③

・・・

・・・

・・・

・・・・・・・・・

・・・

・・・

状態遷移の条件を確認していくことで、仕様記述における誤りや改善可能な点を抽出することができる。以下に指摘例を 2 つ示す。

3/6

指摘１）※１のセルを見ると、「水量」が「－」となっているが、2 行前では、「水量」が「適正」が条件となっている。このことから、※１における条件もれの可能性が指摘される。この場合は実際に条件がもれていた。
指摘２）※２と※３の列を見ると、蓋に関する条件が異なるメンバー名により表現されている。条件にあらわれるメンバー名がゆれている可能性が指摘される。

④での指摘を受けて、要求事項および SLP 記述を修正する。例として、指摘１）および指摘２）を受けて表 1 の記述を修正したものを表 3 に示す。

表 3 SLP による要求事項の記述（修正版）

要求番号
原文

pot-330-41
アイドル中に蓋センサ on となったら、沸騰行為に遷移する。
if <ポットの状態>{アイドル中}
if <蓋>{閉}if <水量>{適正}Do<ポットの状態>{沸騰行為中にせよ}
else
next

SLP 記述
（修正後）

endif
else
next
endif
else
next
endif
・「アイドル」、「沸騰行為」の主語が明記されていないので、「ポットの状態」を明記する。
・原文では水量の条件が述べられていないが、pot-330-12、pot-330-13 ではアイドルと指摘・修正事項

なる条件に「水量が空」であることが述べられており、整合していない。ここでは条件に「水量が適正」であることも必要であり、明記する。
・「蓋センサ on」とあるが、pot-220-11 では「蓋センサが 3sec 以上 on」とあり、条件記述がゆれている。そこで、後者（つまり蓋が閉）に統一する。

以上の手順を反復することにより、要求仕様書の要求事項の欠陥を除去し、改善していくことができる。

５．効果
上述のレビュー手順を、SESSAME「話題沸騰ポット要求仕様書第 7 版」に適用してみたところ、31 回

4/6

の反復で、109 件の指摘事項を抽出することができた。指摘事項の分類を以下の表に示す。第 7 版の仕様書は SESSAME によれば厳密な版とされているが、これに対して 100 件以上の指摘事項があったということは、提案手法の有効性を示すものである。

表 4 指摘事項の分類と指摘箇所数

指摘内容の分類指摘箇所の数

メンバー名もれ22

メンバー名表記のゆれ

11

状態名表記のゆれ

19

状態もれ

8

条件もれ

24

余計な条件

3

煩雑な条件記述

5

条件にあらわれるメンバー名のゆれ

6

余計な状態遷移

6

状態遷移もれ3

状態遷移の非決定性

2

メンバー名

状態名

状態遷移の条件

状態遷移計 109

SPL の文法は、メンバー名と状態名の間の関係を、条件に従って整理して記述させるものである。このことの第 1 の利点は、要求事項の主語の抜けがなくなることである。自然言語のみによる要求仕様書では、主語が抜けていたり不明確であったりすることがバグの原因となっているが、SLP ではこれを防止することができる。第 2 の利点は、メンバー名毎の状態遷移表の作成が可能となることである。
SLP 文法による要求事項の記述と状態遷移表を併用することは、要求仕様書の理解を深め、欠陥を除去する上で効果的である。これは両者が補完的な役割を担っているからであると考えられる。要求仕様書を記述する場合、われわれ人間は、様々な側面から体系立てて記述するのが一般的であり、また、読む場合にもそのように書かれている方が理解しやすい。例えば、正常時と異常時のシナリオを個別に考えることは得意である。しかしながら、これらを同時に考慮して、いきなりシステムの状態遷移表を埋めようとすることはなかなかむずかしい。よって要求事項は、自然言語と SLP 記述によって記述するのがよい。しかしこれだけでは全体的な関係を把握できないので、それを効率よく俯瞰するためには、状態遷移表を用いるのがよい。提案手法では、システムのローカルな振る舞いの記述を SLP 記述で行い、グローバルな整合性の確認を状態遷移表で行うという役割分担が補完的に機能するため、レビューの効率が上がると考えられる（図 3）。

5/6

図 3 SLP によるレビューの利点

6/6