(57)【要約】【課題】ソフトウェア仕様の誤りを機械的に効率よく検出できる仕様誤り検出プログラム、仕様誤り検出装置および仕様誤り検出方法を提供することである。【解決手段】実施形態の仕様誤り検出プログラムは、コンピュータに、ソフトウェア仕様の処理タプルに基づいて、判定の種類に応じた判定式を含む判定式タプルを生成する判定式タプル生成部１１の機能と、ソフトウェア仕様のデータタプルと処理タプルとに基づいて、ソフトウェア仕様の全体を１つの論理式で表現した論理式化仕様を生成する論理式化仕様生成部１２の機能と、論理式化仕様と１つの判定式とを結合して充足可能性問題情報を生成する充足可能性問題情報生成部１３の機能と、充足可能性問題情報に対する充足可能性の判定結果に基づいて、ソフトウェア仕様の誤りを検出する誤り検出部１４の機能と、を実現させる。【選択図】図４
2018060465.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアで実現する処理と処理に入出力するデータの定義を表したソフトウェア仕様の誤りを検出するための仕様誤り検出プログラムであって、
前記ソフトウェア仕様は、処理に入出力するデータの定義を表すデータタプルと、入力されたデータから出力されるデータを決定する処理を表現した処理タプルと、を含み、
コンピュータに、
前記処理タプルに基づいて、判定の種類に応じた判定式を含む判定式タプルを生成する判定式タプル生成部の機能と、
前記データタプルと前記処理タプルとに基づいて、前記ソフトウェア仕様の全体を１つの論理式で表現した論理式化仕様を生成する論理式化仕様生成部の機能と、
前記論理式化仕様と１つの前記判定式とを結合して充足可能性問題情報を生成する充足可能性問題情報生成部の機能と、
前記充足可能性問題情報に対する充足可能性の判定結果に基づいて、前記ソフトウェア仕様の誤りを検出する誤り検出部の機能と、を実現させるための仕様誤り検出プログラム。
【請求項２】
前記処理タプルは、処理から出力されるデータを表す出力データに対し、処理に入力されるデータに対する条件と該条件が成立するときの処理データの値を示す算出式との組み合わせを１以上対応付けたタプルである、請求項１に記載の仕様誤り検出プログラム。
【請求項３】
前記判定式タプル生成部は、１つの前記処理タプルの全ての条件を論理和で結合して否定を付したものを、前記処理タプルの条件がいずれも成立しないことがないことを保証する十分性を判定するための判定式とし、該判定式と、該判定式が前記十分性を判定する判定式であることを示す情報と、前記処理タプルを示す情報と、を対応付けた前記判定式タプルを生成する、請求項２に記載の仕様誤り検出プログラム。
【請求項４】
前記誤り検出部は、前記充足可能性問題情報に含まれる前記判定式が前記十分性を判定するための判定式であれば、前記充足可能性問題情報に対する充足可能性の判定結果が充足可能である場合に、前記判定式に対応する前記処理タプルに前記十分性の違反に相当する誤りがあると判断する、請求項３に記載の仕様誤り検出プログラム。
【請求項５】
前記判定式タプル生成部は、１つの前記処理タプルの１つの条件を、成立しない条件が１つもないことを保証する到達性を判定するための判定式とし、該判定式と、該判定式が到達性を判定する判定式であることを示す情報と、前記処理タプルを示す情報と、を対応付けた前記判定式タプルを生成する、請求項２乃至４のいずれか一項に記載の仕様誤り検出プログラム。
【請求項６】
前記誤り検出部は、前記充足可能性問題情報に含まれる前記判定式が前記到達性の違反を判定するための判定式であれば、前記充足可能性問題情報に対する充足可能性の判定結果が充足不可能である場合に、前記判定式に対応する前記処理タプルに前記到達性の違反に相当する誤りがあると判断する、請求項５に記載の仕様誤り検出プログラム。
【請求項７】
前記判定式タプル生成部は、１つの前記処理タプルの２つの条件を論理積で結合したものを、１つの前記処理タプルの２つの条件が同時に成立することがないことを保証する決定性を判定するための判定式とし、該判定式と、該判定式が前記決定性の違反を判定する判定式であることを示す情報と、前記処理タプルを示す情報と、を対応付けた前記判定式タプルを生成する、請求項２乃至６のいずれか一項に記載の仕様誤り検出プログラム。
【請求項８】
前記誤り検出部は、前記充足可能性問題情報に含まれる前記判定式が前記決定性を判定するための判定式であれば、前記充足可能性問題情報に対する充足可能性の判定結果が充足可能である場合に、前記判定式に対応する前記処理タプルに前記決定性の違反に相当する誤りがあると判断する、請求項７に記載の仕様誤り検出プログラム。
【請求項９】
前記データタプルは、データの名前を表すデータ名に対し、該データが取り得る値の範囲を表す定義域を対応付けたタプルであり、
前記論理式化仕様生成部は、前記ソフトウェア仕様に含まれる全ての前記データタプルの定義域と、全ての前記処理タプルの全ての条件と算出式との組み合わせとを論理積で結合して前記論理式化仕様を生成する、請求項２乃至８のいずれか一項に記載の仕様誤り検出プログラム。
【請求項１０】
ソフトウェアで実現する処理と処理に入出力するデータの定義を表したソフトウェア仕様の誤りを検出する仕様誤り検出装置であって、
前記ソフトウェア仕様は、処理に入出力するデータの定義を表すデータタプルと、入力されたデータから出力されるデータを決定する処理を表現した処理タプルと、を含み、
前記処理タプルに基づいて、判定の種類に応じた判定式を含む判定式タプルを生成する判定式タプル生成部と、
前記データタプルと前記処理タプルとに基づいて、前記ソフトウェア仕様の全体を１つの論理式で表現した論理式化仕様を生成する論理式化仕様生成部と、
前記論理式化仕様と１つの前記判定式とを結合して充足可能性問題情報を生成する充足可能性問題情報生成部と、
前記充足可能性問題情報に対する充足可能性の判定結果に基づいて、前記ソフトウェア仕様の誤りを検出する誤り検出部と、を備える仕様誤り検出装置。
【請求項１１】
ソフトウェアで実現する処理と処理に入出力するデータの定義を表したソフトウェア仕様の誤りを検出する仕様誤り検出方法であって、
前記ソフトウェア仕様は、処理に入出力するデータの定義を表すデータタプルと、入力されたデータから出力されるデータを決定する処理を表現した処理タプルと、を含み、
前記処理タプルに基づいて、判定の種類に応じた判定式を含む判定式タプルを生成するステップと、
前記データタプルと前記処理タプルとに基づいて、前記ソフトウェア仕様の全体を１つの論理式で表現した論理式化仕様を生成するステップと、
前記論理式化仕様と１つの前記判定式とを結合して充足可能性問題情報を生成するステップと、
前記充足可能性問題情報に対する充足可能性の判定結果に基づいて、前記ソフトウェア仕様の誤りを検出するステップと、を含む仕様誤り検出方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、仕様誤り検出プログラム、仕様誤り検出装置および仕様誤り検出方法に関する。
【背景技術】
【０００２】
信頼性や安全性が求められるシステムにおいては、出荷後に不具合が発生しないように開発段階でその品質を保証していくことが重要である。このような中、ソフトウェア開発における仕様の作成段階では、一般的に人手のレビューによって仕様の正しさが検証されている。しかし近年、ソフトウェアに求められる機能の増加により、仕様の規模と複雑さが増大している。このため、人手によるレビューの品質を一定に保つことが難しく、また必要となるコストも高まる。こうした背景から、ソフトウェア仕様の誤りを機械的に（つまり、人手によらずに）効率よく検出して、ソフトウェア仕様の検証作業にかかるコストを低減する仕組みの構築が望まれている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特許第５４６０６２９号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
本発明が解決しようとする課題は、ソフトウェア仕様の誤りを機械的に効率よく検出できる仕様誤り検出プログラム、仕様誤り検出装置および仕様誤り検出方法を提供することである。
【課題を解決するための手段】
【０００５】
実施形態の仕様誤り検出プログラムは、ソフトウェアで実現する処理と処理に入出力するデータの定義を表したソフトウェア仕様の誤りを検出するためのプログラムである。前記ソフトウェア仕様は、処理に入出力するデータの定義を表すデータタプルと、入力されたデータから出力されるデータを決定する処理を表現した処理タプルと、を含む。実施形態の仕様誤り検出プログラムは、コンピュータに、判定式タプル生成部の機能と、論理式化仕様生成部の機能と、充足可能性問題情報生成部の機能と、誤り検出部の機能と、を実現させる。判定式タプル生成部は、前記処理タプルに基づいて、判定の種類に応じた判定式を含む判定式タプルを生成する。論理式化仕様生成部は、前記データタプルと前記処理タプルとに基づいて、前記ソフトウェア仕様の全体を１つの論理式で表現した論理式化仕様を生成する。充足可能性問題情報生成部は、前記論理式化仕様と１つの前記判定式とを結合して充足可能性問題情報を生成する。誤り検出部は、前記充足可能性問題情報に対する充足可能性の判定結果に基づいて、前記ソフトウェア仕様の誤りを検出する。
【図面の簡単な説明】
【０００６】
【図１】図１は、ソフトウェア仕様の具体例を示す図である。
【図２】図２は、ソフトウェア仕様における到達性の違反、決定性の違反、および十分性の違反の具体例を示す図である。
【図３】図３は、実施形態の仕様誤り検出装置のハードウェア構成例を示すブロック図である。
【図４】図４は、実施形態の仕様誤り検出装置の機能的な構成例を示すブロック図である。
【図５】図５は、到達性の判定式タプルを生成する例を説明する図である。
【図６】図６は、決定性の判定式タプルを生成する例を説明する図である。
【図７】図７は、十分性の判定式タプルを生成する例を説明する図である。
【図８】図８は、判定式タプル群の具体例を示す図である。
【図９】図９は、判定式タプル群の具体例を示す図である。
【図１０】図１０は、論理式化仕様を生成する処理を説明する図である。
【図１１】図１１は、充足可能性問題情報を生成する処理を説明する図である。
【図１２】図１２は、仕様の誤りを検出する処理を説明する図である。
【図１３】図１３は、仕様誤り結果タプル群の具体例を示す図である。
【図１４】図１４は、仕様誤り結果が「有」の仕様誤り結果タプル群の具体例を示す図である。
【図１５】図１５は、実施形態の仕様誤り検出装置による処理手順の一例を示すフローチャートである。
【図１６】図１６は、ソフトウェア仕様をテキスト形式で記述した例を示す図である。
【図１７】図１７は、ＳＭＴソルバの入力形式で生成された論理式化仕様の一例を示す図である。
【図１８】図１８は、ＳＭＴソルバの入力形式で生成された充足可能性問題情報の一例を示す図である。
【図１９】図１９は、ＳＭＴソルバから出力される充足可能性判定結果の一例を示す図である。
【図２０】図２０は、充足可能性判定結果に基づき仕様誤り結果タプルを生成する処理を説明する図である。
【図２１】図２１は、実施形態の効果を説明する図である。
【発明を実施するための形態】
【０００７】
以下、実施形態の仕様誤り検出プログラム、仕様誤り検出装置および仕様誤り検出方法を、図面を参照して詳細に説明する。
【０００８】
＜実施形態の概要＞
まず、本実施形態の概要について説明する。本実施形態は、ソフトウェア仕様の誤りを機械的に効率よく検出して、ソフトウェア仕様の検証作業にかかるコスト低減に寄与するものである。特に、本実施形態では、ソフトウェア仕様の全体を通した論理的な誤りを多面的に検出できるようにしている。
【０００９】
ここで、本実施形態で扱うソフトウェア仕様について説明する。ソフトウェア仕様は、ソフトウェアで実現する処理と処理に入出力するデータの定義を表したものである。本実施形態で扱うソフトウェア仕様は、表形式によって表現可能なものであり、図１に示すように、データタプルの集合であるデータタプル群Ｄ１と、処理タプルの集合である処理タプル群Ｄ２とで構成される。図１の例は、温度設定モードと設定温度とから求まる目標温度と、計測温度に補正値を掛けた補正温度とに基づいて、ヒータのオン／オフ（Ｔｒｕｅ／Ｆａｌｓｅ）を制御するソフトウェアの仕様を表している。
【００１０】
データタプル群Ｄ１を構成する各データタプルは、処理に入出力するデータの定義を表現したタプルであり、データ名と定義域とを持つ。データ名は、そのデータの名前を表す。定義域は、そのデータが取り得る値の範囲を表した式である。つまり、データタプルは、データの名前を表すデータ名に対し、該データが取り得る値の範囲を表す定義域を対応付けたタプルである。
【００１１】
処理タプル群Ｄ２を構成する各処理タプルは、入力されたデータから出力されるデータを決定する処理を表現したタプルであり、出力データと、条件と算出式の組とを持つ。出力データは、処理から出力されるデータを表す。条件は、入力されたデータの値をもとに真偽（条件が成立する／しない）を判定する論理式である。算出式は、入力されたデータから出力データの値を算出する式である。条件が真になるとき、「出力データ＝算出式」の関係が成立する。条件と算出式の組は、１つの処理タプルに対して１以上持つ。つまり、処理タプルは、処理から出力されるデータを表す出力データに対し、処理に入力されるデータに対する条件と該条件が成立するときの処理データの値を示す算出式との組み合わせを１以上対応付けたタプルである。なお、処理タプルは、条件が、真偽を問わないことを示す“ｄｏｎ‘ｔ  ｃａｒｅ”を持つ場合もある。図１に示す処理タプル群Ｄ２のうち、出力データ「補正温度」の処理タプルがその一例である。
【００１２】
このようなソフトウェア仕様では、ある処理タプルの出力データが他の処理タプルの条件や算出式中のデータで使われるとき、その処理タプル間に入出力の関係があることを示している。また、処理タプルの条件や算出式中のデータが他の処理タプルの出力データで使用されていないとき、そのデータはシステムの外部から入力されることを示している。
【００１３】
本実施形態では、ソフトウェア仕様全体を充足可能性問題（ＳＡＴ）として捉え、それを解くことで仕様の論理的な正しさを判定する。充足可能性問題は、与えられた命題論理に対して真偽の存在を判定する問題であり、充足可能性を判定するソフトウェアとして、数多くのＳＡＴソルバやこれを拡張したＳＭＴソルバが、フリーソフトとして公開されている。本実施形態では、充足可能性の判定自体はこうしたソルバ（特に、真偽値以外も扱うことができるＳＭＴソルバ）を利用するものとし、検証の対象となるソフトウェア仕様をもとにソルバに入力する情報（以下、「充足可能性問題情報」という）を生成し、この充足可能性問題情報に対してソルバから出力される充足可能性の判定結果に基づいて、ソフトウェア仕様の誤りを検出する。
【００１４】
ここで、仕様が論理的に正しいとは、あらゆる入力を入れても出力の値が必ず一意に決まり、また、仕様の中に実行されない記述がないこと、と捉えることができる。ここで、仕様の論理的な正しさを処理タプルの条件に着目して考えると、成立しない条件が１つもないこと（以下、この性質を「到達性」という）、２つの条件が同時に成立することがないこと（以下、この性質を「決定性」という）、条件がいずれも成立しないことがないこと（以下、この性質を「十分性」という）が全て保証される場合に、仕様が論理的に正しいと判定できる。本実施形態では、これら到達性、決定性および十分性といった多面的な観点で、ソフトウェア仕様の誤りを検出する。
【００１５】
ソフトウェア仕様における到達性の違反、決定性の違反、および十分性の違反の具体例を図２に示す。図２は、図１に示した処理タプル群Ｄ２のうち、出力データが「ヒータ」の処理タプルに注目した例である。
【００１６】
出力データが「ヒータ」の処理タプルには、「目標温度＝１００」という条件が含まれている。しかし、出力データが「目標温度」の処理タプルの算出式からは１００の値が求まらない（図１参照）ため、到達性の違反がある。
【００１７】
また、出力データが「ヒータ」の処理タプルには、算出式「Ｆａｌｓｅ」に対応する「目標温度＜＝４０」という条件と、算出式「Ｔｒｕｅ」に対応する「補正温度＜目標温度」という条件とが含まれている。しかし、補正温度＜目標温度＜＝４０が成立するため、決定性の違反がある。
【００１８】
また、出力データが「補正温度」の処理タプルと、出力データが「目標温度」の処理タプルによると、目標温度と補正温度が同じ値となる場合もある（図１参照）。しかし、出力データが「ヒータ」の処理タプルには、「目標温度＝補正温度」という条件が欠けているため、十分性の違反がある。
【００１９】
本実施形態は、検証の対象となるソフトウェア仕様から、以上のような到達性の違反に相当する誤り、決定性の違反に相当する誤り、および、十分性の違反に相当する誤りを機械的に検出するものである。なお、図２の例において、「目標温度＜補正温度＜＝１００」という条件は、データタプルにおいて「補正温度＜＝１００」であることが定義されているため、「補正温度＜＝１００」の記載部分が冗長である。人手による仕様の作成段階では、実際にこのような冗長な記載が生じ得るが、これはソフトウェア仕様の論理的な正しさに影響を与えないため、本実施形態では誤りとして検出しないものとしている。
【００２０】
＜装置構成＞
図３は、本実施形態の仕様誤り検出装置１０のハードウェア構成例を示すブロック図である。本実施形態の仕様誤り検出装置１０は、例えば、通常のコンピュータとしてのハードウェアを備え、このハードウェアとソフトウェア（仕様誤り検出プログラム）との協働により、ソフトウェア仕様の誤りを検出する処理を行う。
【００２１】
すなわち、本実施形態の仕様誤り検出装置１０は、例えば図３に示すように、情報処理を行うＣＰＵ１０１、ＢＩＯＳなどを記憶した読み出し専用メモリであるＲＯＭ１０２、各種データを書き換え可能に記憶するＲＡＭ１０３、各種のデータやプログラムを格納するＨＤＤ１０４、記憶媒体１１０を用いて情報を保管したり外部に情報を配布したり外部から情報を入手するための媒体駆動装置１０５、ユーザがＣＰＵ１０１に命令や情報などを入力するためのキーボードやマウスなどの入力装置１０６、および、処理経過や結果などをユーザに表示する液晶ディスプレイなどの表示装置１０７などを備え、これら各部間で送受信されるデータをバスコントローラ１０８が調停して動作する。
【００２２】
このようなハードウェア構成を有する仕様誤り検出装置１０では、ユーザが電源を投入するとＣＰＵ１０１がＲＯＭ１０２内のローダーというプログラムを起動させ、ＨＤＤ１０４よりＯＳ（Operating  System）というコンピュータのハードウェアとソフトウェアとを管理するプログラムをＲＡＭ１０３に読み込み、このＯＳを起動させる。このようなＯＳは、ユーザの操作に応じてプログラムを起動したり、情報を読み込んだり、保存を行ったりする。ＯＳのうち代表的なものとしては、Ｗｉｎｄｏｗｓ（登録商標）、ＵＮＩＸ（登録商標）などが知られている。これらのＯＳ上で動作するプログラムをアプリケーションプログラムと呼んでいる。なお、アプリケーションプログラムは、所定のＯＳ上で動作するものに限らず、後述の各種処理の一部の実行をＯＳに肩代わりさせるものであってもよいし、所定のアプリケーションソフトやＯＳなどを構成する一群のプログラムファイルの一部として含まれているものであってもよい。
【００２３】
ここで、本実施形態の仕様誤り検出装置１０は、アプリケーションプログラムとして、本実施形態の仕様誤り検出プログラムをＨＤＤ１０４に記憶している。本実施形態の仕様誤り検出プログラムは、例えば、ＣＤ−ＲＯＭやＤＶＤなどの各種の光ディスク、各種光磁気ディスク、フレキシブルディスクなどの各種磁気ディスク、半導体メモリなどの各種方式のメディアなどの記憶媒体１１０に記録されて提供され、ＨＤＤ１０４にインストールされる。また、本実施形態の仕様誤り検出プログラムは、例えばネットワークを利用した通信により外部からダウンロードされ、ＨＤＤ１０４にインストールされてもよい。
【００２４】
以上のようなハードウェア構成を採用する場合、ＣＰＵ１０１がＯＳ上で動作する仕様誤り検出プログラムに従って各種の演算処理を実行することにより、コンピュータを本実施形態の仕様誤り検出装置１０として動作させて、後述の機能的な構成要素をコンピュータ上で実現させることができる。なお、本実施形態の仕様誤り検出プログラムは、上述したように、充足可能性問題情報の充足可能性を判定するために、例えばフリーソフトとして提供されているソルバを利用する。このソルバは、本実施形態の仕様誤り検出プログラムと同様に予めＨＤＤ１０４にインストールされていてもよいし、ソルバを利用する際にその都度取得して一時的に保持するようにしてもよい。また、仕様誤り検出装置１０の内部にソルバを取り込まず、充足可能性問題情報を外部のソルバに渡して判定を依頼し、その判定結果を取得する構成としてもよい。
【００２５】
なお、本実施形態では、仕様誤り検出装置１０を構成する後述の機能的な構成要素の全てをコンピュータ上で実現することを想定するが、これら機能的な構成要素の一部あるいは全部を、例えば、ＡＳＩＣ（Application  Specific  Integrated  Circuit）やＦＰＧＡ（Field  Programmable  Gate  Array）などの専用のハードウェアを用いて実現することもできる。
【００２６】
また、本実施形態では、仕様誤り検出装置１０が単体の装置として構成されていることを想定するが、仕様誤り検出装置１０は単体の装置として構成されている必要はなく、物理的に分離されてネットワークを介して接続された複数の装置により構成されていてもよい。また、仕様誤り検出装置１０は、例えば、クラウドシステム上で動作する仮想マシンとして実現されていてもよい。
【００２７】
図４は、本実施形態の仕様誤り検出装置１０の機能的な構成例を示すブロック図である。本実施形態の仕様誤り検出装置１０は、上述の仕様誤り検出プログラムを実行することにより実現される機能的な構成要素として、判定式タプル生成部１１と、論理式化仕様生成部１２と、充足可能性問題情報生成部１３と、誤り検出部１４とを備える。
【００２８】
判定式タプル生成部１１は、ソフトウェア仕様を構成する処理タプル群Ｄ２に含まれる各処理タプルに基づいて、その処理タプルに対する到達性、決定性、十分性の判定に用いる判定式を含む判定式タプルを生成する。判定式タプルは、処理タプルに対する到達性、決定性、十分性のいずれか１つを判定するための判定式と、その判定式が到達性、決定性、十分性のいずれを判定する式であるかを表す判定式の種類と、その判定式の対象となる処理タプルを表す処理タプル情報と、を対応付けたタプルである。
【００２９】
判定式タプル生成部１１は、ソフトウェア仕様の処理タプル群Ｄ２に含まれる全ての処理タプルについて、処理タプルに対する到達性の判定式を含む判定式タプル（到達性の判定式タプル）、処理タプルに対する決定性の判定式を含む判定式タプル（決定性の判定式タプル）、処理タプルに対する十分性の判定式を含む判定式タプル（十分性の判定式タプル）をそれぞれ生成する。判定式タプル生成部１１が生成したこれらの判定式タプルの集合が、図４に示す判定式タプル群Ｄ３である。なお、ソフトウェア仕様の処理タプル群Ｄ２に含まれる処理タプルの中には、判定式タプルが生成されない（生成できない）ものもある。
【００３０】
処理タプルに対する到達性の判定式は、その処理タプルの１つの条件をそのまま取り出したものである。判定式タプル生成部１１は、１つの処理タプルの１つの条件（個々の条件）を取得して到達性を判定するための判定式とする。そして、その判定式に対し、その判定式が到達性を判定する判定式であることを示す判定式の種類と、その判定式の対象となる処理タプルを表す処理タプル情報（例えば、処理タプルの出力データ）とを対応付けて、到達性の判定式タプルを生成する。
【００３１】
図５は、図１に示した処理タプル群Ｄ２のうち、出力データが「ヒータ」の処理タプルについて到達性の判定式タプルを生成する例を示す図である。出力データが「ヒータ」の処理タプルは、「目標温度＜＝４０」、「補正温度＜目標温度」、「目標温度＜補正温度＜＝１００」、および「目標温度＝１００」の４つの条件を持つ。判定式タプル生成部１１は、これら４つの条件をそれぞれ取得して到達性を判定する４つの判定式とし、各判定式に対して処理タプル情報「ヒータ」と、判定式の種類「到達性」とを対応付けた４つの判定式タプルを、出力データが「ヒータ」の処理タプルに対する到達性の判定式タプルとして生成する。
【００３２】
処理タプルに対する決定性の判定式は、その処理タプルの２つの条件を論理積で結合したものである。判定式タプル生成部１１は、１つの処理タプルの２つの条件を取得して論理積で結合することで、決定性を判定するための判定式を生成する。そして、その判定式に対し、その判定式が決定性を判定する判定式であることを示す判定式の種類と、その判定式の対象となる処理タプルを表す処理タプル情報とを対応付けて、決定性の判定式タプルを生成する。
【００３３】
図６は、図１に示した処理タプル群Ｄ２のうち、出力データが「ヒータ」の処理タプルについて決定性の判定式タプルを生成する例を示す図である。出力データが「ヒータ」の処理タプルは、上述のように「目標温度＜＝４０」、「補正温度＜目標温度」、「目標温度＜補正温度＜＝１００」、および「目標温度＝１００」の４つの条件を持つ。したがって、これら４つの条件のうちの２つの条件の組み合わせは６通りある。判定式タプル生成部１１は、これら６通りの組み合わせのそれぞれについて、一方の条件と他方の条件とを論理積（∧）で結合したものを、決定性を判定する６つの判定式とし、各判定式に対して処理タプル情報「ヒータ」と、判定式の種類「決定性」とを対応付けた６つの判定式タプルを、出力データが「ヒータ」の処理タプルに対する決定性の判定式タプルとして生成する。
【００３４】
処理タプルに対する十分性の判定式は、その処理タプルの全ての条件を論理和で結合して否定を付したものである。判定式タプル生成部１１は、１つの処理タプルの全ての条件を取得して論理和で結合し、否定を付すことにより十分性を判定するための判定式を生成する。そして、その判定式に対し、その判定式が十分性を判定する判定式であることを示す判定式の種類と、その判定式の対象となる処理タプルを表す処理タプル情報とを対応付けて、十分性の判定式タプルを生成する。
【００３５】
図７は、図１に示した処理タプル群Ｄ２のうち、出力データが「ヒータ」の処理タプルについて十分性の判定式タプルを生成する例を示す図である。出力データが「ヒータ」の処理タプルは、上述のように「目標温度＜＝４０」、「補正温度＜目標温度」、「目標温度＜補正温度＜＝１００」、および「目標温度＝１００」の４つの条件を持つ。判定式タプル生成部１１は、これら４つの条件を全て論理和（∨）で結合して否定（¬）を付したものを、十分性を判定する判定式とし、その判定式に対して処理タプル情報「ヒータ」と、判定式の種類「十分性」とを対応付けた判定式タプルを、出力データが「ヒータ」の処理タプルに対する十分性の判定式タプルとして生成する。
【００３６】
図８は、図１に示した処理タプル群Ｄ２のうち、出力データが「ヒータ」の処理タプルについて、到達性、決定性、十分性の全ての判定式タプルを生成した結果である判定式タプル群の具体例を示す図である。出力データが「ヒータ」の処理タプルは４つの条件を持つため、この処理タプルを対象とした判定式タプル生成部１１の処理により、４つの到達性の判定式タプルと、６つの決定性の判定式タプルと、１つの十分性の判定式タプルとが生成され、１１個の判定式タプルを含む判定式タプル群が得られる。
【００３７】
図９は、図１に示した処理タプル群Ｄ２の全体に対して判定式タプルを生成した結果である判定式タプル群Ｄ３の具体例を示す図である。図１に示した処理タプル群Ｄ２のうち、出力データが「補正温度」の処理タプルは、条件が上述の“ｄｏｎ‘ｔ  ｃａｒｅ”を表す「−」のみであるため、判定式タプルは生成されない。出力データが「目標温度」の処理タプルは３つの条件を持つため、この処理タプルを対象とした判定式タプル生成部１１の処理により、３つの到達性の判定式タプルと、３つの決定性の判定式タプルと、１つの十分性の判定式タプルとが生成される。したがって、上述の出力データが「ヒータ」の処理タプルに対する１１個の判定式タプルと、出力データが「目標温度」の処理タプルに対する７個の判定式タプルとを含む判定式タプル群が得られる。
【００３８】
図９に示す判定式タプル群は、検証の対象となるソフトウェア仕様を構成する処理タプル群Ｄ２の全体に対して判定式タプルを生成した結果であり、これが図４の判定式タプル群Ｄ３となる。判定式タプル群Ｄ３は、このソフトウェア仕様に対する処理が終了するまで、例えば図３に示したＨＤＤ１０４など、本実施形態の誤り検出装置１０の内部の記憶装置に保持される。
【００３９】
論理式化仕様生成部１２は、ソフトウェア仕様を構成するデータタプル群Ｄ１（データタプル）と、ソフトウェア仕様を構成する処理タプル群Ｄ２（処理タプル）とに基づいて、論理式化仕様を生成する。論理式化仕様は、ソフトウェア仕様の全体を１つの論理式で表現したものである。論理式化仕様生成部１２は、例えば、データタプル群Ｄ１に含まれる全てのデータタプルの定義域と、処理タプル群Ｄ２に含まれる全ての処理タプルにおける全ての条件と算出式との組み合わせ（ここでは、条件と算出式との組み合わせを「条件⇒出力データ＝算出式」の論理式で表現する）とを論理積で結合して、論理式化仕様を生成する。
【００４０】
図１０は、論理式化仕様を生成する処理を説明する図であり、図１に示したデータタプル群Ｄ１と処理タプル群Ｄ２とに基づいて論理式化仕様を生成する例を示している。論理式化仕様生成部１２は、データタプル群Ｄ１に含まれる全てのデータタプルの定義域を取得するとともに、処理タプル群Ｄ２に含まれる全ての処理タプルの全ての条件と算出式との組み合わせを取得する。ここで、処理タプルの条件と算出式との組み合わせは、「条件⇒出力データ＝算出式」の論理式（論理記号「⇒」は含意を表す）に変形される。そして、論理式化仕様生成部１２は、全てのデータタプルの定義域を表す式と、「条件⇒出力データ＝算出式」の論理式に変形した全ての処理タプルの全ての条件と算出式との組み合わせを論理積（∧）で結合し、図１０に示すような論理式化仕様を生成する。論理式化仕様生成部１２が生成した論理式化仕様は、充足可能性問題情報生成部１３に渡される。
【００４１】
充足可能性問題情報生成部１３は、論理式化仕様生成部１２が生成した論理式化仕様と、判定式タプル群Ｄ３に含まれる１つの判定式タプルの判定式とを結合して、ソルバ２０に入力する情報である充足可能性問題情報を生成する。充足可能性問題情報は、ソフトウェア仕様を充足可能性問題と捉えてその充足可能性を判定するための論理式である。充足可能性問題情報生成部１３は、判定式タプル群Ｄ３に含まれる全ての判定式タプルについて、充足可能性問題情報を生成する処理を繰り返す。したがって、充足可能性問題情報は判定式タプル群Ｄ３に含まれる判定式タプルの数だけ生成され、それぞれの充足可能性問題情報に対して充足可能性が判定される。
【００４２】
図１１は、充足可能性問題情報を生成する処理を説明する図であり、図１０に示した論理式化仕様に対して、判定式「目標温度＜＝４０」を論理積（∧）で結合して充足可能性問題情報を生成する例を示している。充足可能性問題情報生成部１３は、判定式タプル群Ｄ３に含まれる各判定式タプルから判定式を順次取得し、取得した判定式を論理式化仕様に論理積で結合することで、それぞれの判定式に対応する充足可能性問題情報を順次生成する。充足可能性問題情報生成部１３が生成した充足可能性問題情報は、誤り検出部１４に渡される。
【００４３】
誤り検出部１４は、充足可能性問題情報生成部１３が生成した充足可能性問題情報に対する充足可能性の判定結果に基づいて、ソフトウェア仕様の誤りを検出する処理を行う。すなわち、誤り検出部１４は、充足可能性問題情報生成部１３から充足可能性問題情報が渡されると、ソルバ２０を呼び出して、充足可能性問題情報をソルバ２０に入力する。そして、ソルバ２０から出力される充足可能性判定結果（充足可能性問題情報に対する充足可能または充足不可能の情報）と、充足可能性問題情報に含まれる判定式の種類（例えば判定式タプルを参照して特定できる）とに基づいて、論理的な誤りの有無を判定する。
【００４４】
具体的には、誤り検出部１４は、ソルバ２０から出力される充足可能性判定結果と、充足可能性問題情報に含まれる判定式の種類とが、以下に示すパターン（１）〜（３）のいずれかに当てはまる場合に、そのパターンに対応する論理的な誤りがあると判断する。
パターン（１）：判定式の種類＝到達性、充足可能性判定結果＝充足不可能
→判定式に対応する処理タプルに到達性の違反に相当する誤りがあると判断する。
パターン（２）：判定式の種類＝決定性、充足可能性判定結果＝充足可能
→判定式に対応する処理タプルに決定性の違反に相当する誤りがあると判断する。
パターン（３）：判定式の種類＝十分性、充足可能性判定結果：充足可能
→判定式に対応する処理タプルに十分性の違反に相当する誤りがあると判断する。
【００４５】
誤り検出部１４は、充足可能性問題情報生成部１３が生成した充足可能性問題情報のそれぞれについて上述の処理を繰り返し、それぞれの充足可能性問題情報について、仕様誤り結果タプルを生成する。仕様誤り結果タプルは、仕様誤りの有無を示す仕様誤り結果と、充足可能性問題情報に含まれる判定式を持つ判定式タプルを示す判定式タプル情報とを対応付けたタプルである。誤り検出部１４が生成したこれらの仕様誤り結果タプルの集合が、図４に示す仕様誤り結果タプル群Ｄ４である。
【００４６】
図１２は、仕様の誤りを検出する処理を説明する図であり、図１１に示した充足可能性問題情報に対する充足可能性の判定結果に基づいて、論理的な誤りの有無を判定する例を示している。この図１２の例では、充足可能性問題情報に含まれる判定式の種類は「到達性」であり、充足可能性問題情報に対する充足可能性判定結果は「充足可能」である。この判定式の種類と充足可能性判定結果の組み合わせは上記のパターン（１）〜（３）のいずれにも当てはまらないため、誤り検出部１４は、この判定式によって検出される仕様の誤りは無いと判断し、仕様誤り結果を「無」とした仕様誤り結果タプルを生成する。
【００４７】
図１３は、図９に示した判定式タプル群Ｄ３に含まれる判定式タプルを各々用いて生成された全ての充足可能性問題情報に対して、誤り検出部１４が上述の処理を繰り返し実施することで得られる仕様誤り結果タプル群Ｄ４の具体例を示す図である。また、図１４は、図１３に示す仕様誤り結果タプル群Ｄ４のうち、仕様誤り結果が「有」の仕様誤り結果タプルを抜き出したものである。
【００４８】
図１３および図１４に示す例では、図１に示したデータタプル群Ｄ１および処理タプル群Ｄ２から構成されるソフトウェア仕様の論理的な仕様の誤りとして、４つの誤りが検出されたことを示している。１つ目の誤りは、出力データが「ヒータ」の処理タプルについて、「目標温度＝１００」の条件が成立しないという到達性の違反を示している。２つ目の誤りは、出力データが「ヒータ」の処理タプルについて、「目標温度＜＝４０」と「補正温度＜目標温度」の２つの条件が同時に成立するという決定性の違反を示している。３つ目の誤りは、出力データが「ヒータ」の処理タプルについて、「目標温度＜＝４０」と「目標温度＜補正温度＜＝１００」の２つの条件が同時に成立するという決定性の違反を示している。４つ目の誤りは、出力データが「ヒータ」の処理タプルについて、「目標温度＜＝４０」、「補正温度＜目標温度」、「目標温度＜補正温度＜＝１００」、「目標温度＝１００」以外の条件が成立するという十分性の違反を示している。
【００４９】
本実施形態の仕様誤り検出装置１０は、図１３に示したような仕様誤り結果タプル群Ｄ４、あるいは図１４に示したような仕様誤り結果が「有」の仕様誤り結果タプルを出力することで、ソフトウェア仕様の検証を行う作業者にソフトウェア仕様の論理的な誤りを認識させる。これにより、ソフトウェア仕様の検証作業にかかるコストを低減させることができる。本実施形態の仕様誤り検出装置１０の出力は、図３に示した表示装置１０７による表示であってもよいし、ネットワークを利用した通信により外部装置に表示させる形態であってもよい。また、図１３に示したような仕様誤り結果タプル群Ｄ４、あるいは図１４に示したような仕様誤り結果が「有」の仕様誤り結果タプルを図３に示したＨＤＤ１０４などに保存しておき、ソフトウェア仕様の検証を行う作業者が必要に応じて参照できるようにしてもよい。
【００５０】
＜動作説明＞
次に、以上のように構成される本実施形態の仕様誤り検出装置１０の動作の概要を図１５に沿って説明する。図１５は、本実施形態の仕様誤り検出装置１０による処理手順の一例を示すフローチャートである。仕様誤り検出装置１０は、図１５に示すステップＳ１０１からステップＳ１０９の処理を順次実行して、ソフトウェア仕様の誤りを検出する。
【００５１】
ステップＳ１０１：本実施形態の仕様誤り検出装置１０による処理が開始されると、まず、判定式タプル生成部１１が、検証の対象となるソフトウェア仕様を構成する処理タプル群Ｄ２から処理タプルを１つ取り出して、次のステップＳ１０２に進む。
【００５２】
ステップＳ１０２：判定式タプル生成部１１が、ステップＳ１０１で取り出した処理タプルに基づいて、上述した方法により到達性の判定式タプル、決定性の判定式タプル、および十分性の判定式タプルをそれぞれ生成し、次のステップＳ１０３に進む。なお、上述の出力データが「補正温度」の処理タプルなど、判定式タプルが生成されない処理タプルについてはステップＳ１０２の処理がスキップされる。
【００５３】
ステップＳ１０３：判定式タプル生成部１１が、処理タプル群Ｄ２に含まれる全ての処理タプルを取り出したか否かを判定する。そして、処理タプル群Ｄ２に含まれる全ての処理タプルを取り出していれば（ステップＳ１０３：Ｙｅｓ）、次のステップＳ１０４に進み、取り出していない処理タプルがあれば（ステップＳ１０３：Ｎｏ）、ステップＳ１０１に戻って以降の処理を繰り返す。
【００５４】
ステップＳ１０４：論理式化仕様生成部１２が、検証の対象となるソフトウェア仕様を構成するデータタプル群Ｄ１と、処理タプル群Ｄ２とに基づいて、上述した方法により論理式化仕様を生成し、次のステップＳ１０５に進む。
【００５５】
ステップＳ１０５：充足可能性問題情報生成部１３が、ステップＳ１０２で生成された判定式タプルの集合である判定式タプル群Ｄ３から判定式タプルを１つ取り出し、次のステップＳ１０６に進む。
【００５６】
ステップＳ１０６：充足可能性問題情報生成部１３が、ステップＳ１０４で生成された論理式化仕様とステップＳ１０５で取り出した判定式タプルに含まれる判定式とを論理積で結合して充足可能性問題情報を生成し、次のステップＳ１０７に進む。
【００５７】
ステップＳ１０７：誤り検出部１４が、ソルバ２０を呼び出してステップＳ１０６で生成された充足可能性問題情報を入力し、充足可能性問題情報に対する充足可能性判定結果を取得して、次のステップＳ１０８に進む。
【００５８】
ステップＳ１０８：誤り検出部１４が、ステップＳ１０７でソルバ２０に入力した充足可能性問題情報に含まれる判定式の種類と、ステップＳ１０７で取得した充足可能性判定結果とに基づいて、ソフトウェア仕様の誤りの有無を判定する。そして、判定結果に応じた仕様誤り結果タプルを生成し、次のステップＳ１０９に進む。
【００５９】
ステップＳ１０９：誤り検出部１４が、判定式タプル群Ｄ３に含まれる全ての判定式タプルに対する処理が終了したか否かを判定する。そして、判定式タプル群Ｄ３に含まれる全ての判定式タプルに対する処理が終了していれば（ステップＳ１０９：Ｙｅｓ）、次のステップＳ１１０に進み、未処理の判定式タプルがあれば（ステップＳ１０９：Ｎｏ）、ステップＳ１０５に戻って以降の処理を繰り返す。
【００６０】
ステップＳ１１０：仕様誤り検出装置１０は、ステップＳ１０８で生成された仕様誤り結果タプルの集合である仕様誤り結果タプル群Ｄ４、あるいは、この仕様誤り結果タプル群Ｄ４のうち仕様誤り結果が「有」の仕様誤り結果タプルを出力して、一連の処理を終了する。
【００６１】
＜実施例＞
次に、充足可能性問題情報の充足可能性を判定するソルバ２０として、ＳＭＴソルバの１つであるＺ３（“Z3  Theorem  Provers”（https://github.com/Z3Prover）参照）を利用する場合を例に挙げて、より具体的な実施例を説明する。
【００６２】
本実施例では、ＳＭＴソルバの入力形式を想定して、上述のデータタプル群Ｄ１と処理タプル群Ｄ２とで構成されるソフトウェア仕様をテキスト形式で記述する。図１に示したソフトウェア仕様をテキスト形式で記述した例を図１６に示す。テキスト形式で記述したソフトウェア仕様では、データタプル群Ｄ１に含まれる各データタプルが「データ名：｛定義域｝」の形で表され、処理タプル群Ｄ２に含まれる各処理タプルが「出力データ＝case｛条件−＞算出式；…｝」の形で表されている。
【００６３】
図１７は、ＳＭＴソルバの入力形式で生成された論理式化仕様の一例を示す図である。ここでは型宣言が必要な場合を想定し、論理式化仕様の前に型宣言の記述がある。型宣言では、データタプル群Ｄ１に含まれる各データタプルのデータ名が（declare-const  データ名  型）で表されている。また、論理式化仕様では、データタプル群Ｄ１に含まれる各データタプルの定義域が（assert  （定義域））で表され、処理タプル群Ｄ２に含まれる各処理タプルの「条件⇒出力データ＝算出式」の論理式が、（assert（＝＞（条件）（＝処理結果  算出式）））の形式で表されている。これらassert文は、論理積で結合されていることと等しい意味を持つ。なお、データタプルの定義域、処理タプルの条件や算出式などはポーランド記法で表す。また、入力形式上、データ名を英数字へ置き換える処理も施す。
【００６４】
図１８は、ＳＭＴソルバの入力形式で生成された充足可能性問題情報の一例を示す図である。図１７に示した論理式化仕様に対して１つの判定式を論理積で結合することで、図１８に示す充足可能性問題情報が生成される。判定式は、ＳＭＴソルバの入力形式、具体的には（assert  （条件））の形式に置き換えられて論理式化仕様に結合される。このとき、ＳＭＴソルバの入力に必要なコマンド（check-sat，get-model）の追加も行われる。このように生成された充足可能性問題情報をＳＭＴソルバに入力することで、充足可能性判定結果が得られる。
【００６５】
図１９は、ＳＭＴソルバから出力される充足可能性判定結果の一例を示す図である。充足可能性判定結果は、図１９に示すような形式でＳＭＴソルバから出力される。判定結果は、充足可能であればｓａｔ、充足不可能であればｕｎｓａｔとなる。また、判定結果が充足可能（ｓａｔ）であれば、そのときの具体例も示される。
【００６６】
図２０は、充足可能性判定結果に基づき仕様誤り結果タプルを生成する処理を説明する図である。図２０の例では、充足可能性判定結果が充足可能、判定式の種類が到達性であるため、仕様に誤りが無いと判定される。そして、仕様誤り結果「無」と充足可能性問題情報の生成に用いた判定式タプルを示す判定式タプル情報とを対応付けた仕様誤り結果タプルが生成される。
【００６７】
＜実施形態の効果＞
以上、具体例を挙げながら詳細に説明したように、本実施形態の仕様誤り検出装置１０によれば、ソフトウェア仕様の誤りを機械的に効率よく検出することができ、ソフトウェア仕様の検証作業にかかるコストを低減させることができる。
【００６８】
特に、本実施形態の仕様誤り検出装置１０は、ソフトウェア仕様の論理的な正しさに関して、到達性の違反、決定性の違反、および、十分性の違反といったように、多面的に誤りを検出できるようにしているので、ソフトウェア仕様の誤りを精度よく検出することができる。例えば、十分性の違反の検出は、検証の対象となるソフトウェア仕様の抜けや漏れを検出するものである。仕様の誤りを検出する従来の技術では、与えられた仕様が正しいかどうかを判定することはできても、仕様の抜けや漏れを検出することができなかった。これに対し、本実施形態の仕様誤り検出装置１０によれば、こういった仕様の抜けや漏れについても機械的に検出することができる。
【００６９】
また、本実施形態の仕様誤り検出装置１０は、ソフトウェア仕様全体を充足可能性問題として捉え、それを解くことで仕様の論理的な正しさを判定するようにしている。つまり、ソフトウェア仕様を１つの論理式で表した論理式化仕様に対して、到達性、決定性、十分性を判定する判定式を１つ結合して充足可能性問題情報を生成し、この充足可能性問題情報に対する充足可能性の判定結果に基づいて、判定式の種類に応じたソフトウェア仕様の誤りを検出している。したがって、ソフトウェア仕様全体を通した到達性の誤り、決定性の誤り、十分性の誤りを適切に検出することができる。
【００７０】
これまで、命題形式の仕様における命題間の矛盾を見つけるために２つの条件を充足可能性問題として判定する試みはあった。しかし、この従来技術では、２つの処理の繋がりについては考慮されておらず、一方の処理の結果を用いた条件によって他方の処理の結果が決まるような仕様については、誤りを適切に検出できない場合があった。図２１を用いて具体的に説明すると、従来技術では、図２１（ａ）に示すように、結果Ｅが、結果Ｃを用いた条件によって決まるような仕様を想定していない。このため、図２１（ｂ）に示す決定性の違反、到達性の違反、十分性の違反といった仕様の誤りを検出することができない。これに対し、本実施形態の仕様誤り検出装置１０によれば、図２１（ｂ）に示す決定性の違反、到達性の違反、十分性の違反といった仕様の誤りを適切に検出することができる。
【００７１】
以上、本発明の実施形態を説明したが、ここで説明した実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。ここで説明した新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。ここで説明した実施形態やその変形は、発明の範囲や要旨に含まれるとともに、請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【００７２】
１０  仕様誤り検出装置
１１  判定式タプル生成部
１２  論理式化仕様生成部
１３  充足可能性問題情報生成部
１４  誤り検出部
２０  ソルバ
Ｄ１  データタプル群
Ｄ２  処理タプル群
Ｄ３  判定式タプル群
Ｄ４  仕様誤り結果タプル群
【図１】
2018060465.tif 000003
【図２】
2018060465.tif 000004
【図３】
2018060465.tif 000005
【図４】
2018060465.tif 000006
【図５】
2018060465.tif 000007
【図６】
2018060465.tif 000008
【図７】
2018060465.tif 000009
【図８】
2018060465.tif 000010
【図９】
2018060465.tif 000011
【図１０】
2018060465.tif 000012
【図１１】
2018060465.tif 000013
【図１２】
2018060465.tif 000014
【図１３】
2018060465.tif 000015
【図１４】
2018060465.tif 000016
【図１５】
2018060465.tif 000017
【図１６】
2018060465.tif 000018
【図１７】
2018060465.tif 000019
【図１８】
2018060465.tif 000020
【図１９】
2018060465.tif 000021
【図２０】
2018060465.tif 000022
【図２１】
2018060465.tif 000023