(57)【特許請求の範囲】
【請求項１】
形式言語によってソフトウェアの仕様を記述した第１の形式モデル記述に、未確定の仕様の追記を定義する追記定義情報を入力する追記定義情報入力部、
入力した前記追記定義情報に応じて、前記第１の形式モデル記述に未確定仕様記述を挿入し、第２の形式モデル記述を作成する未確定仕様記述挿入部、
入出力装置を介した指示に応答して、前記第２の形式モデル記述に挿入された前記未確定仕様記述を、否定的仕様記述および肯定的仕様記述のいずれか一方に置換し、第３の形式モデル記述を作成する仕様記述置換部、および
形式言語と自然言語との変換表を用いて、前記第３の形式モデル記述から、前記ソフトウェアの自然言語仕様記述を抽出するソフトウェア仕様記述抽出部を有することを特徴とするソフトウェア仕様抽出装置。
【請求項２】
前記仕様記述置換部は、前記指示が前記未確定仕様記述の前記否定的仕様記述への置換の指示のとき、前記否定的仕様記述への置換を、前記未確定仕様記述を処理として実行されないコメント文とすることを特徴とする請求項１に記載のソフトウェア仕様抽出装置。
【請求項３】
前記ソフトウェア仕様記述抽出部は、前記第３の形式モデル記述からの前記自然言語仕様記述の抽出に対応して、該抽出に用いた前記変換表の前記形式言語と前記自然言語との対応関係情報を保持し、
さらに、前記自然言語仕様記述の箇所の削除および編集禁止のいずれか一方の指示入力に応答して、前記指示入力が削除のとき、前記対応関係情報を参照して前記自然言語仕様記述の箇所に対応する前記第３の形式モデル記述の箇所を削除し、前記指示入力が編集禁止のとき、前記対応関係情報を参照して前記自然言語仕様記述の箇所に対応する前記第３の形式モデル記述の箇所に編集禁止を示すコメント文を挿入するソフトウェア仕様記述編集部を有することを特徴とする請求項１に記載のソフトウェア仕様抽出装置。
【請求項４】
さらに、前記入出力装置からの編集指示に応じて、前記編集禁止を示すコメント文が挿入された前記第３の形式モデル記述の箇所への編集処理をブロックし、前記第３の形式モデル記述を対象に、前記肯定的仕様記述の追加または削除、前記否定的仕様記述の追加または削除、前記未確定仕様記述の前記肯定的仕様記述への置換、および前記未確定仕様記述の否定的仕様記述への置換のいずれか一つの編集処理を実行する形式モデル記述編集部を有することを特徴とする請求項３に記載のソフトウェア仕様抽出装置。
【請求項５】
前記形式モデル記述編集部は、前記肯定的仕様記述および前記否定的仕様記述のいずれか一方を削除した後、前記未確定仕様記述挿入部を再実行させ、
前記未確定仕様記述挿入部は、前記肯定的仕様記述および前記否定的仕様記述のいずれか一方を前記未確定仕様記述へ置換することを特徴とする請求項４に記載のソフトウェア仕様抽出装置。
【請求項６】
ソフトウェア仕様抽出装置におけるソフトウェア仕様抽出方法であって、前記ソフトウェア仕様抽出装置は、
形式言語によってソフトウェアの仕様を記述した第１の形式モデル記述に、未確定の仕様の追記を定義する追記定義情報を入力し、
入力した前記追記定義情報に応じて、前記第１の形式モデル記述に未確定仕様記述を挿入して、第２の形式モデル記述を作成し、
入出力装置を介した指示に応答して、前記第２の形式モデル記述に挿入された前記未確定仕様記述を、否定的仕様記述および肯定的仕様記述のいずれか一方に置換して、第３の形式モデル記述を作成し、
形式言語と自然言語との変換表を用いて、前記第３の形式モデル記述から、前記ソフトウェアの自然言語仕様記述を抽出することを特徴とするソフトウェア仕様抽出方法。
【請求項７】
前記ソフトウェア仕様抽出装置は、前記指示が前記未確定仕様記述の前記否定的仕様記述への置換の指示のとき、前記否定的仕様記述への置換を、前記未確定仕様記述を処理として実行されないコメント文とすることを特徴とする請求項６に記載のソフトウェア仕様抽出方法。
【請求項８】
前記ソフトウェア仕様抽出装置は、前記第３の形式モデル記述からの前記自然言語仕様記述の抽出に対応して、該抽出に用いた前記変換表の前記形式言語と前記自然言語との対応関係情報を保持し、
前記自然言語仕様記述の箇所の削除および編集禁止のいずれか一方の指示入力に応答して、前記指示入力が削除のとき、前記対応関係情報を参照して前記自然言語仕様記述の箇所に対応する前記第３の形式モデル記述の箇所を削除し、前記指示入力が編集禁止のとき、前記対応関係情報を参照して前記自然言語仕様記述の箇所に対応する前記第３の形式モデル記述の箇所に編集禁止を示すコメント文を挿入することを特徴とする請求項６に記載のソフトウェア仕様抽出方法。
【請求項９】
前記ソフトウェア仕様抽出装置は、前記入出力装置からの編集指示に応じて、前記編集禁止を示すコメント文が挿入された前記第３の形式モデル記述の箇所への編集処理をブロックし、前記第３の形式モデル記述を対象に、前記肯定的仕様記述の追加または削除、前記否定的仕様記述の追加または削除、前記未確定仕様記述の前記肯定的仕様記述への置換、および前記未確定仕様記述の否定的仕様記述への置換のいずれか一つの編集処理を実行することを特徴とする請求項８に記載のソフトウェア仕様抽出方法。
【請求項１０】
前記ソフトウェア仕様抽出装置は、前記肯定的仕様記述および前記否定的仕様記述のいずれか一方を削除した後、削除に対応した前記肯定的仕様記述および前記否定的仕様記述のいずれか一方を前記未確定仕様記述へ置換することを特徴とする請求項９に記載のソフトウェア仕様抽出方法。
【請求項１１】
形式言語によってソフトウェアの仕様を記述した第１の形式モデル記述に、未確定の仕様の追記を定義する追記定義情報を入力する追記定義情報入力部、
入力した前記追記定義情報に応じて、前記第１の形式モデル記述に未確定仕様記述を挿入し、第２の形式モデル記述を作成する未確定仕様記述挿入部、
入出力装置を介した指示に応答して、前記第２の形式モデル記述に挿入された前記未確定仕様記述を、否定的仕様記述および肯定的仕様記述のいずれか一方に置換し、第３の形式モデル記述を作成する仕様記述置換部、および
形式言語と自然言語との変換表を用いて、前記第３の形式モデル記述から、前記ソフトウェアの自然言語仕様記述を抽出するソフトウェア仕様記述抽出部として、ソフトウェア仕様抽出装置を機能させることを特徴とするソフトウェア仕様抽出プログラム。
【請求項１２】
前記仕様記述置換部は、前記指示が前記未確定仕様記述の前記否定的仕様記述への置換の指示のとき、前記否定的仕様記述への置換を、前記未確定仕様記述を処理として実行されないコメント文とすることを特徴とする請求項１１に記載のソフトウェア仕様抽出プログラム。
【請求項１３】
前記ソフトウェア仕様記述抽出部は、前記第３の形式モデル記述からの前記自然言語仕様記述の抽出に対応して、該抽出に用いた前記変換表の前記形式言語と前記自然言語との対応関係情報を保持し、
さらに、前記自然言語仕様記述の箇所の削除および編集禁止のいずれか一方の指示入力に応答して、前記指示入力が削除のとき、前記対応関係情報を参照して前記自然言語仕様記述の箇所に対応する前記第３の形式モデル記述の箇所を削除し、前記指示入力が編集禁止のとき、前記対応関係情報を参照して前記自然言語仕様記述の箇所に対応する前記第３の形式モデル記述の箇所に編集禁止を示すコメント文を挿入するソフトウェア仕様記述編集部として、前記ソフトウェア仕様抽出装置を機能させることを特徴とする請求項１１に記載のソフトウェア仕様抽出プログラム。
【請求項１４】
さらに、前記入出力装置からの編集指示に応じて、前記編集禁止を示すコメント文が挿入された前記第３の形式モデル記述の箇所への編集処理をブロックし、前記第３の形式モデル記述を対象に、前記肯定的仕様記述の追加または削除、前記否定的仕様記述の追加または削除、前記未確定仕様記述の前記肯定的仕様記述への置換、および前記未確定仕様記述の否定的仕様記述への置換のいずれか一つの編集処理を実行する形式モデル記述編集部として、前記ソフトウェア仕様抽出装置を機能させることを特徴とする請求項１３に記載のソフトウェア仕様抽出プログラム。
【請求項１５】
前記形式モデル記述編集部は、前記肯定的仕様記述および前記否定的仕様記述のいずれか一方を削除した後、再実行指示を発行し、その再実行指示により、削除に対応した前記肯定的仕様記述および前記否定的仕様記述のいずれか一方を前記未確定仕様記述へ置換する前記未確定仕様記述挿入部として、前記ソフトウェア仕様抽出装置を機能させることを特徴とする請求項１４に記載のソフトウェア仕様抽出プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアシステム開発を支援する技術に関し、特に、ソフトウェアシステムを構成するソフトウェアの仕様を抽出する技術に関する。
【背景技術】
【０００２】
ソフトウェアシステムの不具合の原因の一つに、設計したソフトウェアの仕様誤りがある。仕様誤りを検出するためには、形式手法による検証が有効である。形式手法によるソフトウェア仕様の検証は、数学的意味を持つ形式言語を用いてソフトウェア仕様を記述し、形式言語で記述されたソフトウェア仕様記述（以下、形式モデル記述と呼ぶ）の正しさを、数学的手法に基づいて証明することで行われる。
【０００３】
一般に、形式モデル記述は、自然言語で記述された仕様（自然言語仕様記述）から変換表を用いた変換により生成される。特許文献１は、自然言語仕様記述を形式モデル記述に変換する際に、自然言語仕様記述では記述されていない仕様を推論によって導出し、導出した仕様に対応する形式モデル記述を補完する方法を開示している。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２０１３−８４０２３号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
ソフトウェアシステム開発においては、ソフトウェア全体の仕様を設計し、設計した全体仕様をブレークダウンして、ソフトウェアを構成するコンポーネントの仕様を設計する。他社や他部署から提供されるソフトウェアパッケージなどの仕様が設計したコンポーネントの仕様に適合すれば、ソフトウェアの開発効率の観点から、ソフトウェアパッケージなどを利用することが一般的である。また、設計したコンポーネントに対応してソフトウェアパッケージを新規に開発することも一般的である。
【０００６】
しかしながら、設計したコンポーネントの仕様にソフトウェアパッケージの仕様が適合すると誤って認識し、その誤った認識に基づいてソフトウェアの仕様を設計することにより、不具合を引き起こすケースが多い。ソフトウェアパッケージの詳細な仕様は入手困難なことも多く、ソフトウェアパッケージの仕様の認識不足や誤認識が発生する可能性がある。
【０００７】
仕様の認識不足や誤認識の可能性があるソフトウェアパッケージを含むソフトウェアの仕様は、設計したソフトウェアの仕様の検証に向けて形式モデル記述を作成するために特許文献１の技術を適用しても、推論によって導出した仕様に対応する形式モデル記述を補完するだけなので、依然として、形式モデル記述のソフトウェアの仕様に認識不足や誤認識の可能性を含むことになる。
【０００８】
換言すると、仕様の認識不足や誤認識の可能性があるコンポーネント（以下では、ソフトウェアパッケージと同義）を含むソフトウェアを形式手法により検証すると、「認識不足や誤認識の可能性があるソフトウェアの仕様に誤りがあるか」を検証することになり、ソフトウェアの仕様の認識不足や認識誤りに起因する、ソフトウェアの不具合を削減できない。
【課題を解決するための手段】
【０００９】
開示するソフトウェア仕様抽出装置は、形式言語によってソフトウェアの仕様を記述した第１の形式モデル記述に、未確定の仕様の追記を定義する追記定義情報を入力する追記定義情報入力部、入力した追記定義情報に応じて、第１の形式モデル記述に未確定仕様記述を挿入し、第２の形式モデル記述を作成する未確定仕様記述挿入部、入出力装置を介した指示に応答して、第２の形式モデル記述に挿入された未確定仕様記述を、否定的仕様記述および肯定的仕様記述のいずれか一方に置換し、第３の形式モデル記述を作成する仕様記述置換部、および、形式言語と自然言語との変換表を用いて、第３の形式モデル記述から、ソフトウェアの自然言語仕様記述を抽出するソフトウェア仕様記述抽出部を有する。
【発明の効果】
【００１０】
開示するソフトウェア仕様抽出装置によれば、ソフトウェアの仕様の認識不足や認識誤りに起因する、ソフトウェアの不具合を削減できる。
【図面の簡単な説明】
【００１１】
【図１】ソフトウェア仕様抽出装置の構成例である。
【図２】形式モデル記述の例である。
【図３】追記定義情報の例である。
【図４】未確定仕様記述挿入部の処理フローチャートである。
【図５】未確定仕様記述挿入部の実行結果としての形式モデル記述の例である。
【図６】仕様記述置換部の処理フローチャートである。
【図７】仕様記述置換部の実行結果としての形式モデル記述の例である。
【図８】ソフトウェアの自然言語仕様記述の例である。
【図９】対応関係情報の例である。
【図１０】ソフトウェアの自然言語仕様記述の例である。
【図１１】ソフトウェア仕様記述編集部の処理フローチャートである。
【図１２】編集禁止のコメント文が挿入された形式モデル記述の例である。
【発明を実施するための形態】
【００１２】
ソフトウェア仕様抽出装置の実施形態を具体的に説明する前に、概要を説明する。ソフトウェア仕様抽出装置は、ソフトウェアのコンポーネントの仕様の認識不足や認識誤りに起因する、ソフトウェアの不具合を削減するために、コンポーネント（ソフトウェア＝コンポーネントの場合もあるので、以下では、ソフトウェア）が満たすべき仕様を明確にする必要がある。そのために、ソフトウェア仕様抽出装置は、次の手順を実行する。
【００１３】
ソフトウェア仕様抽出装置は、自然言語で記述されたソフトウェアの自然言語仕様記述に基づき、自然言語仕様記述と形式モデル記述とを対応させた変換表を用いて、形式モデル記述を作成する。自然言語仕様記述は、ソフトウェアの処理、およびその満たすべき性質を定義している。作成した形式モデル記述を、ソフトウェアには不具合はないという検証結果が得られるように、ソフトウェアの仕様を仮定して変更する。仮定したソフトウェアの仕様の形式モデル記述は、不具合回避のためにソフトウェアに期待すべき仕様を表している。期待すべき仕様とは、たとえば、ソフトウェアの全体仕様を満足するコンポーネントの仕様である。コンポーネントがソフトウェアそのものである場合は、期待すべき仕様はソフトウェアの全体仕様である。ソフトウェアに期待すべき仕様の形式モデル記述から、ソフトウェアに期待すべき自然言語仕様記述を抽出する。抽出された自然言語仕様記述には、形式モデル記述の作成に用いた元の自然言語仕様記述が不具合回避のために変更された形式モデル記述の内容が反映されている。
【００１４】
抽出した自然言語仕様記述の利用は、ソフトウェアのレビューや、ソフトウェアの開発部署やサポート部署への問い合わせを容易にすることになる。抽出したソフトウェアの自然言語仕様記述の利用により、不具合に繋がるようなソフトウェアの仕様の誤認識や認識不足がある(前述した元の自然言語仕様記述に誤りや記述不足がある)場合、誤認識したソフトウェアの仕様を改めることができる。
【００１５】
上記手順では、ソフトウェアの仕様を仮定し、仮定した仕様に基づいて形式モデル記述を作成するが、その際、次のような二次的な課題がある。
【００１６】
ソフトウェアの処理を表す仕様を仮定する場合、「ある処理を実行する」というような処理の存在を肯定する肯定的仕様と、「ある処理を実行しない」というような処理の存在を否定する否定的仕様の２種類の仮定がある。また、それらのいずれの仮定も与えず、「ある処理を実行するかもしれないし、実行しないかもしれない」という処理の存在が未確定な未確定仕様として扱う場合もある。
【００１７】
これらの３種類の仕様を自然言語で表現（自然言語仕様記述）する場合、肯定的仕様および否定的仕様は明示的に記述される必要があり、記述していない仕様は未確定仕様として解釈される。一方、３種類の仕様を形式言語で表現（形式モデル記述）する場合、肯定的仕様および未確定仕様は明示的に記述される必要があり、記述していない仕様は否定的仕様として解釈される。明示的に記述されていない仕様は、自然言語仕様記述の場合は未確定仕様として解釈され、形式モデル記述の場合は否定的仕様として解釈されるという違いがある。そのため、形式モデル記述においてある仕様を記述しなかった場合、その仕様は未確定仕様と解釈されるのではなく、「その処理は存在しない」という否定的仕様に解釈される。
【００１８】
したがって、ソフトウェアの自然言語仕様記述に基づいて形式モデル記述を作成する際には、未確定仕様を表す形式モデル記述を作成する必要がある。しかし、自然言語仕様記述では未確定仕様を記述しないことから、未確定仕様を表す形式モデル記述を漏れなく作成するのは困難である。未確定仕様を表す形式モデル記述に漏れがあった場合、設計者が未確定仕様であると意図した自然言語仕様記述（設計者は意図したものの記述していない）が、形式モデル記述において否定的仕様として解釈される。形式モデル記述のソフトウェアを検証（形式手法による検証）すると、設計者の意図とは異なる、誤りのある検証結果となる。このような形式モデル記述から抽出する自然言語仕様記述にも、誤りがあることになる。
【００１９】
たとえば、ある形式モデル記述において記述箇所（以下、箇所）AとBがあるとする。箇所Aには処理Xが存在しないという否定的仕様を定義したいが、箇所Bには存在する可能性がある処理Xを未確定仕様にしておきたいとする。この場合、箇所Aに「処理Xは存在しない」という否定的仕様を表す記述を明示的に追記するだけでは不十分で、箇所Bに「処理Xが存在するかもしれないし、存在しないかもしれない」という未確定仕様を表す記述を追記しなければならない。箇所Bに未確定の意味を表す記述を追記しないと、形式手法による検証の際に、「箇所Bには処理Xは存在しない」と解釈され、設計者の意図とは異なる仕様の検証結果が得られる。
【００２０】
そこで、ソフトウェア仕様抽出装置は、形式モデル記述に対して、明示的な記述が追記されることを示す追記定義情報を入力する。ソフトウェア仕様抽出装置は、追記定義情報に基づいて、元の自然言語仕様記述から作成した形式モデル記述に、追記の可能性がある箇所と追記の可能性がある処理を抽出する。ソフトウェア仕様抽出装置は、追記の可能性がある、形式モデル記述の箇所に、追記の可能性がある処理の存在が未確定であることを表す未確定仕様記述を追加する。これにより、未確定仕様を表す未確定仕様記述の追加漏れを防止し、ソフトウェアの仕様認識不足や仕様認識誤りに起因する不具合を削減する。
【００２１】
以下、上述した二次的課題も考慮したソフトウェア仕様抽出装置を、図面を参照しながら詳細に説明する。
【００２２】
図１は、ソフトウェア仕様抽出装置１００の構成例である。ソフトウェア仕様抽出装置１００は、追記定義情報入力部１０１、追記定義情報保持部１０２、未確定仕様記述挿入部１０３、形式モデル記述保持部１０４、検証部１０５、形式モデル記述編集部１０６、仕様記述置換部１０７、ソフトウェア仕様記述抽出部１０８、ソフトウェア仕様記述保持部１０９、対応関係情報保持部１１０、およびソフトウェア仕様記述編集部１１１を含む。期待仕様抽出装置は、ＣＰＵ、メモリ、入出力装置を有するコンピュータ上で実現される。上記各処理部は、ＣＰＵによって処理が実行され、各保持部はメモリに設けられる。
【００２３】
追記定義情報入力部１０１は、形式モデル記述のどの箇所にどのような記述が追記され得るか（追記可能性）を表す追記定義情報を入力し、追記定義情報保持部１０２に格納する。
【００２４】
未確定仕様記述挿入部１０３は、追記定義情報保持部１０２に格納されている追記定義情報に基づいて、形式モデル記述保持部１０４に格納されているソフトウェアの形式モデル記述における、追記の可能性がある箇所と、その箇所に追記の可能性がある処理を決定し、追記の可能性がある箇所に、追記の可能性がある処理の存在が未確定であることを表すコメント文を付与する。未確定仕様記述挿入部１０３は、コメント文を付与した形式モデル記述を形式モデル記述保持部１０４に格納する。コメント文が付与される前の形式モデル記述は、肯定的仕様記述と呼ぶ、ソフトウェアの処理およびその満たすべき性質を表す記述を含む。
【００２５】
検証部１０５は、形式モデル記述保持部１０４に格納されている形式モデル記述のソフトウェアの形式手法による検証を実行し、検証結果を出力する。ソフトウェア仕様抽出装置１００は、ソフトウェアの形式手法による検証の対象である形式モデル記述を決定するための装置であるので、検証部１０５の詳細説明を省略する。
【００２６】
形式モデル記述編集部１０６は、入出力装置からの指示に応じて、形式モデル記述保持部１０４に格納されている形式モデル記述を編集する。形式モデル記述を編集には、肯定的仕様記述の追加または削除、否定的仕様記述の追加または削除、未確定仕様記述の肯定的仕様記述への置換、および未確定仕様記述の否定的仕様記述への置換がある。肯定的仕様記述または否定的仕様記述の削除は、未確定仕様記述を肯定的仕様記述または否定的仕様記述に置換した結果を、元の未確定仕様記述に戻すためである。形式モデル記述編集部１０６は、形式モデル記述を削除した後、未確定仕様記述挿入部１０３を再実行させることにより、削除に対応した形式モデル記述を未確定仕様記述に戻す。
【００２７】
なお、形式モデル記述編集部１０６は、後述するソフトウェア仕様記述編集部１１１による、形式モデル記述に含まれるコメント文「/*編集禁止*/」に基づいて、入出力装置からの編集の指示があっても、コメント文のある形式モデル記述の編集をブロックする（編集しない）。
【００２８】
仕様記述置換部１０７は、形式モデル記述保持部１０４に格納されている形式モデル記述の未確定仕様記述を、肯定的仕様記述または否定的仕様記述に置換する。
【００２９】
ソフトウェア仕様記述抽出部１０８は、形式モデル記述と自然言語仕様記述とを対応させた変換表を用いて、形式モデル記述保持部１０４に格納されているソフトウェアの形式モデル記述からソフトウェアの自然言語仕様記述を抽出(作成)し、ソフトウェア仕様記述保持部１０９に格納する。ソフトウェア仕様記述抽出部１０８による自然言語仕様記述を抽出(作成)は変換表を用いた変換処理であるので、詳細を省略する。
【００３０】
また、ソフトウェア仕様記述抽出部１０８は、ソフトウェアの形式モデル記述から自然言語仕様記述を抽出(作成)する際に用いた変換表の、形式モデル記述と自然言語仕様記述との対応関係情報を対応関係情報保持部１１０に格納する。対応関係情報保持部１１０に格納する形式モデル記述と自然言語仕様記述との対応関係情報を後述するので、ソフトウェア仕様記述抽出部１０８が用いる変換表の内容は後述において明らかになる。
【００３１】
ソフトウェア仕様記述編集部１１１は、形式モデル記述保持部１０４に格納されている形式モデル記述の箇所を削除または編集禁止にする。編集禁止指示の場合は、期待仕様記述上で箇所を指定された記述の編集禁止が指示された形式モデル記述の箇所に編集を禁止するコメント文を追加する。このコメント文により、形式モデル記述編集部１０６による形式モデル記述の編集がブロックされる。
【００３２】
図２は、形式モデル記述保持部１０４に格納されている、元の自然言語仕様記述に基づいて作成されたソフトウェアｐの形式モデル記述の例である。元の自然言語仕様記述に基づくソフトウェアの形式モデル記述の作成は、前述のようにソフトウェアの元の自然言語仕様記述に基づき、自然言語仕様記述と形式モデル記述とを対応させた変換表を用いた形式モデル記述の作成であり、詳細を省略する。ここでは、形式言語Promelaによる形式モデル記述を例とする。形式言語Promelaに限らず、ソフトウェアの処理および性質を記述するその他の形式言語で記述した形式モデル記述であってもよい。以下に説明する例は、図２の形式モデル記述の例に対応している。
【００３３】
図３は、追記定義情報の例である。追記定義情報３０１は、追記定義情報入力部１０１により、入出力装置を介して入力され、追記定義情報保持部１０２に格納される。追記定義情報３０１は、対象ソフトウェア３０２、追記箇所３０３、追記内容３０４、および有効／無効指定３０５を含む。
【００３４】
対象ソフトウェア３０２は、形式モデル記述において、追記の可能性があるソフトウェアを示す。図３の追記定義情報３０１は、図２のソフトウェアｐを追記の対象としている。
【００３５】
追記箇所３０３は、対象ソフトウェア３０２において、追記の可能性がある箇所を示す。たとえば、１行目（＃１）の「任意の代入文の直前・直後」は、ソフトウェアｐに含まれる任意の代入文の直前および直後に追記の可能性があることを示す。同様に２行目（＃２）は、ソフトウェアｐに含まれる代入文y=xの直後に、追記の可能性があることを示す。また、５行目（＃５）の「任意の条件分岐」は、ソフトウェアｐに含まれる任意の条件分岐に対して、分岐条件が追記される可能性があることを示す。
【００３６】
追記内容３０４は、追記箇所３０３が示す箇所に追記する可能性のある内容を示す。たとえば、１行目（＃１）の「任意の文」は、「任意の代入文の直前・直後」の箇所に、定義済みの変数の値を更新する任意の文を追記する可能性があることを意味する。同様に２行目（＃２）は、「代入文y=xの直後」の箇所に代入文「x=1;」を追記する可能性があることを意味する。また、５行目（＃５）の「それ以外の場合の分岐」は、「任意の条件分岐」の箇所に、「既存の分岐条件が成立しない場合」を表すelse条件を追記する可能性があることを意味する。
【００３７】
有効／無効指定３０５は、追記定義情報３０１の対象ソフトウェア３０２、追記箇所３０３、および追記内容３０４の各行の情報の有効または無効を設定する。
【００３８】
図４は、未確定仕様記述挿入部１０３の処理フローチャートである。未確定仕様記述挿入部１０３の処理を説明するために、図２、図３及び図５を用いる。図２の形式モデル記述に対して、図３の追記定義情報に基づき、未確定仕様記述挿入部１０３の処理を実行した結果が、図５の形式モデル記述である。図４は、簡略化のために、１箇所の追記箇所への追記処理として図示するが、以下に説明するように追記定義情報３０１の各行に関して処理を実行する。
【００３９】
未確定仕様記述挿入部１０３は、追記定義情報保持部１０２から、有効／無効指定３０５が有効に設定されている追記定義情報３０１を取得する（ステップ４０１）。
【００４０】
未確定仕様記述挿入部１０３は、形式モデル記述保持部１０４に格納されている形式モデル記述を対象に、追記定義情報３０１に含まれる追記箇所３０３および追記内容３０４に基づき、追記の可能性がある箇所および追記する内容を決定する（ステップ４０２）。たとえば、追記定義情報３０１の２行目（＃２）は、有効／無効指定３０５が有効に設定され、追記箇所３０３に「代入文y=x;の直後」を指定しているので、図２の形式モデル記述の代入文２０１の直後を追記の可能性がある箇所として決定し、箇所として決定された代入文２０１の直後に、追記内容３０４の「x=1;」に基づき、代入文「x=1;」が追記される可能性があることを決定する。
【００４１】
未確定仕様記述挿入部１０３は、決定した追記内容に基づき、未確定仕様記述を作成し、作成した未確定仕様記述を、決定した追記箇所に挿入する（ステップ４０３）。具体的には、次の手順で未確定仕様記述を作成する。
【００４２】
追記内容３０４が、追記定義情報３０１の１行目（＃１）や３行目（＃３）のように「任意の文」の場合、定義済みの全ての変数に対して、任意の値を代入する文を未確定仕様記述として作成する。形式言語Promelaの場合、ある変数vに対して任意の変数を代入する関数は、図５の関数５０１のように定義できる。upperには変数vの上限値を、lowerには変数vの下限値を設定する。この関数５０１を使用して、定義済みの変数ごとにその変数に任意の値を代入する文を未確定仕様記述として作成する。たとえば、未確定仕様記述５０３は、追記定義情報３０１の３行目（＃３）「ｘへの任意の代入文の直前」、ここではｘ＝3の直前に基づいて作成した未確定仕様記述である。
【００４３】
追記内容３０４が、追記定義情報３０１の２行目（＃２）や４行目（＃４）のように特定の代入文の場合、その代入文を実行するか否かを選択する文を未確定仕様記述として作成する。形式言語Promelaの場合、選択する文としてif構文を用いて未確定仕様記述を作成する。たとえば、未確定仕様記述５０２は、追記定義情報３０１の２行目（＃２）に基づいて作成した未確定仕様記述である。
【００４４】
追記内容３０４が、追記定義情報３０１の５行目（＃５）、６行目（＃６）、７行目（＃７）、および８行目（＃８）のように、分岐やループの場合は、その分岐条件やループ条件を表す記述が未確定仕様記述になる。また、分岐条件やループ条件が成立する場合に実行する処理も未確定であるため、定義済みの全ての変数に対する任意の代入文を、分岐条件やループ条件の本文（分岐条件やループ条件が成立する場合に実行する処理）とする。たとえば、未確定仕様記述５０４および未確定仕様記述５０５はそれぞれ、追記定義情報３０１の６行（＃６）目および５行目（＃５）に基づいて作成した未確定仕様記述である。これらの未確定仕様記述は、１つのatomic文にまとめてもよい。
【００４５】
未確定仕様記述挿入部１０３は、形式モデル記述に挿入した未確定仕様記述に対して、未確定仕様記述であることを示し、処理として実行されないコメント文（/＊未確定仕様記述＊/）を付与する（ステップ４０４）。
【００４６】
図６は、未確定仕様記述挿入部１０３によって形式モデル記述に挿入された未確定仕様記述を、否定的仕様記述または肯定的仕様記述に置換する仕様記述置換部１０７の処理フローチャートである。図６は、簡略化のために、一つの未確定仕様記述の置換処理として図示するが、以下に説明するように、形式モデル記述に挿入した各未確定仕様記述に関して処理を実行する。
【００４７】
仕様記述置換部１０７は、未確定仕様記述を否定的仕様記述または肯定的仕様記述に置換する指示を入出力装置から入力する（ステップ６０１）。具体的には、未確定仕様記述が挿入された形式モデル記述を入出力装置に画面出力し、出力画面中の未確定仕様記述箇所を特定した、未確定仕様記述を否定的仕様記述または肯定的仕様記述に置換する指示を入力する。また、肯定的仕様記述への置換指示の場合は、未確定仕様記述を置換する肯定的仕様記述を入力する。未確定仕様記述を示すコメント文が付与されている形式モデル記述を肯定的仕様記述とする場合は、肯定的仕様記述を入力しなくてもよい。また、置換指示が入力されない未確定仕様記述もある。
【００４８】
否定的仕様記述への置換指示の入力に応答して、形式モデル記述保持部１０４に格納されている、未確定仕様記述が挿入された形式モデル記述の、特定された箇所の未確定仕様記述を否定的仕様記述に置換する（ステップ６０２）。具体的には、特定された箇所の未確定仕様記述を、処理として実行されないコメント文にすることで、否定的仕様記述とする。未確定仕様記述が分岐条件またはループ条件の場合は、その本文（分岐条件またはループ条件が成立したときに実行する処理）を削除し、コメント文に含めなくてもよい。
【００４９】
肯定的仕様記述への置換指示の入力に応答して、形式モデル記述保持部１０４に格納されている、未確定仕様記述が挿入された形式モデル記述の、特定された箇所の未確定仕様記述を肯定的仕様記述に置換する（ステップ６０３）。具体的には、特定された箇所の未確定仕様記述を、入力された肯定的仕様記述に置換し、未確定仕様記述を示すコメント文を削除する。ただし、未確定仕様記述として記述している分岐条件やループ条件の本文に含まれる未確定仕様記述を、肯定的仕様記述に置換する場合は、その分岐条件やループ条件も肯定的仕様記述に置換する。
【００５０】
図７は、図５の形式モデル記述を対象に、仕様記述置換部１０７を実行した結果の形式モデル記述の例である。図７において、否定的仕様記述７０１は、未確定仕様記述５０３のうち、「random(y、 y_upper、 y_lower);/*未確定仕様記述*/」を、否定的仕様記述に置換した結果である。否定的仕様記述７０２は、未確定仕様記述５０４を、否定的仕様記述に置換した結果である。肯定的仕様記述７０３および肯定的仕様記述７０４は、未確定仕様記述５０５のうち、分岐条件「:: else -> /*未確定仕様記述*/」と、その本文に含まれる「random(x、 x_upper、 x_lower);/*未確定仕様記述*/」を、肯定的仕様記述に置換した結果である。なお、「random(x、 x_upper、 x_lower);/*未確定仕様記述*/」は、入力された肯定的仕様記述「ｘ＝4」に置換されている。否定的仕様７０５は、未確定仕様記述５０５に含まれる「random(y、 y_upper、 y_lower);/*未確定仕様記述*/」を、否定的仕様記述に置換した結果である。
【００５１】
ソフトウェア仕様記述抽出部１０８は、形式モデル記述と自然言語仕様記述とを対応させた変換表を用いて、形式モデル記述保持部１０４に格納されているソフトウェアの形式モデル記述からソフトウェアの自然言語仕様記述を抽出(作成)し、ソフトウェア仕様記述保持部１０９に格納する。変換表を用いた変換処理であるので詳細を省略し、抽出(作成)したソフトウェアの自然言語仕様記述の例を図８に示す。
【００５２】
対応関係情報保持部１１０に格納される、ソフトウェア仕様記述抽出部１０８が用いた変換表の形式モデル記述と自然言語仕様記述との対応関係情報を図９に示す。図９の対応関係情報９０１は、形式モデル記述９０２と自然言語仕様記述９０３とを対応付けて、各々の行とその記述を示している。
【００５３】
図８のソフトウェアの自然言語仕様記述の例は、図７のソフトウェアの形式モデル記述からソフトウェア仕様記述抽出部１０８が作成したものであり、図９が、ソフトウェア仕様記述抽出部１０８が用いた変換表からの対応関係情報であるので、これらの図を用いて、ソフトウェア仕様記述抽出部１０８の処理の一部を説明する。
【００５４】
自然言語仕様記述８０１の「その後、ｙが変更されることはない」は、ソフトウェア仕様記述抽出部１０８が否定的仕様記述７０１の「/*random(y, y_upper, y_lower);否定的仕様記述*/」を自然言語に変換した結果である。この変換に対応して、変換表から得た対応関係情報は、対応関係情報９０１の＃４の行である。
【００５５】
また、自然言語仕様記述８０２の「xが3の場合の分岐は存在しない」は、ソフトウェア仕様記述抽出部１０８が否定的仕様記述７０２の「/*:: x == 3 -> 否定的仕様記述*/」を自然言語に変換した結果である。この変換に対応して、変換表から得た対応関係情報は、対応関係情報９０１の＃６の行である。
【００５６】
さらに、自然言語仕様記述８０３の「xが2以外の場合は，必ず」は、ソフトウェア仕様記述抽出部１０８が肯定的仕様記述７０３の「:: else ->」を自然言語に変換した結果である。この変換に対応して、変換表から得た対応関係情報は、対応関係情報９０１の＃７の行である。
【００５７】
さらに、自然言語仕様記述８０４、８０５も同様であるので、説明を省略する。
【００５８】
なお、図８の「ソフトウェアpは以下の処理を実行する」や「xの値に応じて次の処理を実行する」などの自然言語記述、および、１、２、・・・、(a)、(b)、・・・などのリスト表示記号は、予めテンプレートとして用意しておく。
【００５９】
図８に示す、未確定仕様記述を残し、肯定的仕様または否定的仕様を仮定した、自然言語仕様記述を用いてソフトウェアの仕様を確認することで、仕様の認識不足や誤認識の可能性を低減でき、確認後にソフトウェアを形式手法により検証することにより、ソフトウェアの不具合を削減できる。
【００６０】
また、ソフトウェアの仕様の確認において誤認識などが明確になった場合は、追記定義情報３０１を修正し、ソフトウェア仕様抽出装置１００を再度、動作させることにより、ソフトウェアの不具合の削減効果が向上する。
【００６１】
以下は、ソフトウェア仕様抽出装置１００の使い勝手を増し、さらにソフトウェアの不具合の削減効果を向上させることについて説明する。
【００６２】
図１０は、図８の自然言語仕様記述の文を並べ替えた自然言語仕様記述の例である。自然言語仕様記述の文は、詳細説明を省略するが、自然言語解析および自然言語編集技術を用いて並べ替える。このような並べ替えによって、自然言語仕様記述の可読性が向上し、ソフトウェアの仕様の確認を容易にする。形式モデル記述は、ソフトウェアの構造、特にネスト（入れ子）構造を反映したものであり、図８の自然言語仕様記述のように形式モデル記述を１対１対応に変換したものでは、自然言語としての可読性は高くない。そこで、並べ替えによって、自然言語仕様記述の可読性（自然言語として読みやすい）が向上する。
【００６３】
図１１は、ソフトウェア仕様記述編集部１１１の処理フローチャートである。ソフトウェア仕様記述編集部１１１は、ソフトウェア仕様記述保持部１０９に格納されているソフトウェアの自然言語仕様記述を入出力装置に出力し、出力した自然言語仕様記述（の箇所）に対する削除指示または編集禁止指示を、入出力装置を介して入力する。（ステップ１１０１）。ソフトウェア仕様記述編集部１１１は、入力した指示に含まれる自然言語仕様記述（の箇所）に対応する、対応関係情報保持部１１０から対応関係情報９０１を取得する（ステップ１１０２）。
【００６４】
削除指示の入力に応答して（ステップ１１０３）、ソフトウェア仕様記述編集部１１１は、取得した対応関係情報１０９を参照し、削除を指示された自然言語仕様記述（の箇所）に対応する、形式モデル記述保持部１０４に格納されている形式モデル記述（の箇所）を特定し、特定した形式モデル記述（の箇所）を削除する（ステップ１１０４）。
【００６５】
編集禁止指示の入力に応答して（ステップ１１０３）、ソフトウェア仕様記述編集部１１１は、取得した対応関係情報１０９を参照し、編集禁止を指示された自然言語仕様記述（の箇所）に対応する、形式モデル記述保持部１０４に格納されている形式モデル記述（の箇所）を特定し、特定した形式モデル記述（の箇所）に編集禁止を意味するコメント文を挿入する（ステップ１１０５）。
【００６６】
図１２は、編集禁止のコメント文が挿入された形式モデル記述の例である。図１２は、図７の形式モデル記述の「ｙ＝5；」に、コメント文を挿入し、「ｙ＝5；/  *編集禁止*/」１２０１とした例である。このコメント文の挿入により、形式モデル記述編集部１０６による形式モデル記述の箇所１２０１の編集がブロックされる。
【００６７】
本実施形態によれば、パッケージ製品を初めとする仕様がブラックボックス化されたコンポーネントを含むソフトウェアシステム開発において、不具合を回避するためにソフトウェアに期待すべき仕様を抽出できるようになるので、ソフトウェアの仕様認識不足や仕様認識誤りに起因する不具合を削減できる。
【００６８】
また本実施形態によれば、一般に形式モデル記述では記述されない否定的仕様を未確定仕様として記述し、コメント文を追加することにより、対応する自然言語仕様記述に、否定的仕様を表す自然言語仕様記述を生成できる。
【００６９】
さらに本実施形態によれば、パッケージ製品を初めとする仕様がブラックボックス化されたソフトウェアを含むソフトウェアシステム開発において、不具合を回避するためにソフトウェアに期待すべき仕様として、ある処理の存在を肯定する肯定的仕様だけでなく、ある処理の存在を否定する否定的仕様も抽出できるようになるので、ソフトウェアの仕様認識不足や仕様認識誤りのうち、特に処理の存在忘れに起因する不具合を削減できる。
【００７０】
さらに本実施形態によれば、ソフトウェアの自然言語仕様記述に誤認を見出した場合に、自然言語仕様記述を修正し、その修正結果を反映した形式モデル記述の再検証が可能であるので、効率的に不具合を検知できる。
【符号の説明】
【００７１】
１００：ソフトウェア仕様抽出装置、１０１：追記定義情報入力部、１０２：追記定義情報保持部、１０３：未確定仕様記述挿入部、１０４：形式モデル記述保持部、１０５：検証部、１０６：形式モデル記述編集部、１０７：仕様記述置換部、１０８：ソフトウェア仕様記述抽出部、１０９：ソフトウェア仕様記述保持部、１１０：対応関係情報保持部、１１１：ソフトウェア仕様記述編集部。
【図１】
0006268062.tif 000002
【図２】
0006268062.tif 000003
【図３】
0006268062.tif 000004
【図４】
0006268062.tif 000005
【図５】
0006268062.tif 000006
【図６】
0006268062.tif 000007
【図７】
0006268062.tif 000008
【図８】
0006268062.tif 000009
【図９】
0006268062.tif 000010
【図１０】
0006268062.tif 000011
【図１１】
0006268062.tif 000012
【図１２】
0006268062.tif 000013