(57)【要約】  ソフトウェアシステムを検証するための方法および装置が開示される。一実施形態では、データ処理装置（１００）が、処理ユニット（１０２）と、処理ユニット（１０２）に通信可能に結合されたメモリユニット（１０４）とを含む。メモリユニット（１０４）は、シミュレーションモジュール（１１６）および検証モジュール（１１８）を含む。シミュレーションモジュール（１１６）は、第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行するように構成される。検証モジュール（１１８）は、ソフトウェアシステムの検証を開始すべきソフトウェアシステムの状態を瞬時に決定するように構成される。検証モジュール（１１８）は、決定された状態においてソフトウェアシステムの検証を開始し、第２の入力値セットに基づいて、第２のステップセットについてソフトウェアシステムの検証を実行し、ソフトウェアシステムの検証の結果を表示ユニット（１１０）に出力するように構成される。
2022502774.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアシステムを検証するためのデータ処理装置（１００）であって、該データ処理装置（１００）が、
少なくとも１つの処理ユニット（１０２）と、
前記処理ユニット（１０２）に通信可能に結合された少なくとも１つのメモリユニット（１０４）と
を備え、前記メモリユニット（１０４）が、
第１の入力値セットに基づいて、第１のステップセットについて前記ソフトウェアシステムのシミュレーションを実行するように構成されたシミュレーションモジュール（１１６）と、
検証モジュール（１１８）であって、
前記ソフトウェアシステムの検証を開始すべき前記ソフトウェアシステムの状態を決定し、
決定された前記状態において前記ソフトウェアシステムの検証を開始し、
第２の入力値セットに基づいて、第２のステップセットについて前記ソフトウェアシステムの検証を実行し、
前記ソフトウェアシステムの前記検証の結果を表示ユニット（１１０）に出力する
ように構成された、検証モジュール（１１８）と
を備える、データ処理装置（１００）。
【請求項２】
前記検証モジュール（１１８）が、前記ソフトウェアシステムをテストするための複数のテストベクタを生成するように構成されている、請求項１記載のデータ処理装置（１００）。
【請求項３】
前記シミュレーションモジュール（１１６）が、閉ループシミュレーション技法を用いて前記ソフトウェアシステムの前記シミュレーションを実行するように構成されている、請求項１または２記載のデータ処理装置（１００）。
【請求項４】
前記検証モジュール（１１８）が、有界モデル検査技法を用いて前記ソフトウェアシステムの前記検証を実行するように構成されている、請求項１または２記載のデータ処理装置（１００）。
【請求項５】
前記シミュレーションモジュール（１１６）が、
前記ソフトウェアシステムにより実行される前記第１のステップセット中に、前記ソフトウェアシステムに関連する一連の状態を決定し、
前記ソフトウェアシステムの各状態に関連する状態変数の値を検証データベースに記憶する
ように構成されている、請求項１から４までのいずれか１項記載のデータ処理装置（１００）。
【請求項６】
前記検証モジュール（１１８）は、
前記ソフトウェアシステムが動作モードで動作し始める状態を前記一連の状態から瞬時に決定する
ように構成されている、請求項１から５までのいずれか１項記載のデータ処理装置（１００）。
【請求項７】
前記検証モジュール（１１８）が、
決定された前記状態に関連する前記状態変数の値を用いて、決定された前記状態において前記ソフトウェアシステムを初期化し、
初期化された前記ソフトウェアシステムの検証を決定された前記状態において開始する
ように構成されている、請求項１から６までのいずれか１項記載のデータ処理装置（１００）。
【請求項８】
前記検証モジュール（１１８）が、
前記ソフトウェアシステムに関連するプログラミング言語文を解析し、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成し、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定する
ように構成されている、請求項１から７までのいずれか１項記載のデータ処理装置（１００）。
【請求項９】
ソフトウェアシステムを検証する方法であって、該方法が、
データ処理装置（１００）により、第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行することと、
前記データ処理装置（１００）により、前記ソフトウェアシステムの検証を開始すべき前記ソフトウェアシステムの状態を決定することと、
前記データ処理装置（１００）により、決定された前記状態において前記ソフトウェアシステムの検証を開始することと、
前記データ処理装置（１００）により、第２の入力値セットに基づいて、第２のステップセットについて前記ソフトウェアシステムの検証を実行することと、
前記データ処理装置（１００）により、前記ソフトウェアシステムの前記検証の結果を表示ユニット（１１０）に出力することと
を含む、方法。
【請求項１０】
前記方法が、前記データ処理装置（１００）により、前記ソフトウェアシステムをテストできる複数のテストベクタを生成することをさらに含む、請求項９記載の方法。
【請求項１１】
前記ソフトウェアシステムの前記シミュレーションが、閉ループシミュレーション技法を用いて実行される、請求項９または１０記載の方法。
【請求項１２】
前記ソフトウェアシステムの前記検証が、有界モデル検査技法を用いて実行される、請求項９または１０記載の方法。
【請求項１３】
前記ソフトウェアシステムの前記シミュレーションを実行することが、
前記ソフトウェアシステムにより実行される前記第１のステップセット中に、前記ソフトウェアシステムに関連する一連の状態を決定することと、
前記ソフトウェアシステムの各状態に関連する状態変数の値を検証データベース（１２０）に記憶することと
を含む、請求項９から１２までのいずれか１項記載の方法。
【請求項１４】
前記ソフトウェアシステムの前記検証を開始すべき前記ソフトウェアシステムの前記状態を決定することが、
前記ソフトウェアシステムが動作モードで動作し始める状態を前記一連の状態から決定すること
を含む、請求項９から１３までのいずれか１項記載の方法。
【請求項１５】
決定された前記状態において前記ソフトウェアシステムの前記検証を開始することが、
決定された前記状態に関連する前記状態変数の値を用いて、決定された前記状態において前記ソフトウェアシステムを初期化することと、
初期化された前記ソフトウェアシステムの検証を決定された前記状態において開始することと
を含む、請求項９から１４までのいずれか１項記載の方法。
【請求項１６】
前記ソフトウェアシステムの前記検証を実行することが、
前記ソフトウェアシステムに関連するプログラミング言語文を解析することと、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成することと、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定することと
を含む、請求項９から１５までのいずれか１項記載の方法。
【請求項１７】
非一時的なコンピュータ可読記憶媒体であって、機械可読命令を記憶しており、前記機械可読命令は、処理ユニット（１０２）により実行される際に、前記処理ユニット（１０２）に、
第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行することと、
前記ソフトウェアシステムの検証を開始すべき前記ソフトウェアシステムの状態を決定することと、
決定された前記状態において前記ソフトウェアシステムの検証を開始することと、
第２の入力値セットに基づいて、第２のステップセットについて前記ソフトウェアシステムの検証を実行することと、
前記ソフトウェアシステムの前記検証の結果を表示ユニットに出力することと
を含む方法を実行させるためのものである、記憶媒体。
【請求項１８】
前記機械可読命令は、前記処理ユニット（１０２）に、
前記ソフトウェアシステムをテストできる複数のテストベクタを生成すること
を含む方法ステップを実行させるためのものである、請求項１７記載の記憶媒体。
【請求項１９】
前記機械可読命令は、前記処理ユニット（１０２）に、
前記ソフトウェアシステムに関連するプログラミング言語文を解析することと、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成することと、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定することと
を含む方法ステップを実行させるためのものである、請求項１７または１８記載の記憶媒体。
【請求項２０】
前記ソフトウェアシステムの前記シミュレーションが、閉ループシミュレーション技法を用いて実行され、前記ソフトウェアシステムの前記検証が、有界モデル検査技法を用いて実行される、請求項１７から１９までのいずれか１項記載の記憶媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本開示は、概してソフトウェアシステムの設計および開発の分野に関し、より詳細にはソフトウェアシステムを検証するための方法および装置に関する。
【０００２】
リアクティブシステムなどのソフトウェアシステムは、ソフトウェアロジックを用いて各ステップで入力データを処理し、出力コマンドを生成する。リアクティブシステムの例は、車両用のアダプティブクルーズコントローラである。アダプティブクルーズコントローラは、次の車両との距離、車両の現在の速度、望ましい速度などの入力データを受け取り、スロットルへの出力コマンドを生成する。
【０００３】
ソフトウェアシステムの開発後、ソフトウェアシステムには、仕様およびソフトウェアシステムの期待される挙動への適合性をリアルタイムで確認するための検証が必要とされる。しかし、ソフトウェアシステムの挙動を網羅的にテストすることは、膨大な数の入力データの長いトレースおよび膨大な時間を必要とするので、現実的ではない。今日では、ソフトウェアシステムの検証が、閉ループシミュレーションを用いて実行される。この技法では、ソフトウェアシステムがリアルタイムで遭遇するであろう典型的なシナリオをカバーする多くのシミュレーションがソフトウェアシステム上で実行される。しかし、閉ループシミュレーションを用いたソフトウェアシステムの検証は、用いるシナリオの数が限られるので、非常に限られた範囲しかカバーできず、かなりの数の検出漏れにつながる。
【０００４】
したがって、ソフトウェアシステムを検証するための方法および装置を開示する。一態様では、ソフトウェアシステムを検証するためのデータ処理装置が、処理ユニットと、処理ユニットに通信可能に結合されたメモリユニットとを含む。メモリユニットは、第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステム（例えば、リアクティブシステム）のシミュレーションを実行するように構成されたシミュレーションモジュールを含む。例えば、ソフトウェアシステムのシミュレーションは、閉ループシミュレーション技法を用いて実行される。メモリユニットは、ソフトウェアシステムの検証を開始すべきソフトウェアシステムの状態を決定し、決定された状態においてソフトウェアシステムの検証を開始するように構成された、検証モジュールを含む。検証モジュールは、第２の入力値セットおよびソフトウェアシステムの一定の内部状態に基づいて、第２のステップセットについてソフトウェアシステムの検証を実行し、ソフトウェアシステムの検証の結果を表示ユニットに出力するように構成されている。例えば、ソフトウェアシステムの検証は、有界モデル検査技法を用いて実行される。さらに、検証モジュールは、ソフトウェアシステムをテストするための複数のテストベクタを生成するように構成されている。第１のステップセットは第２のステップセットよりも大きく、一方で、第１の入力値セットは第２の入力値セットよりも小さいと言える。
【０００５】
加えて、シミュレーションモジュールは、ソフトウェアシステムにより実行される第１のステップセット中に、ソフトウェアシステムに関連する一連の状態を決定し、ソフトウェアシステムの各状態に関連する状態変数の値を検証データベースに記憶するように構成されていてよい。
【０００６】
さらに、検証モジュールは、ソフトウェアシステムが動作モードで動作し始める状態を一連の状態から瞬時に決定するように構成されている。加えて、検証モジュールは、決定された状態に関連する状態変数の値を用いて、決定された状態においてソフトウェアシステムを初期化し、初期化されたソフトウェアシステムの検証を決定された状態において開始するように構成される。
【０００７】
さらに、検証モジュールは、ソフトウェアシステムに関連するプログラミング言語文を解析し、解析されたプログラミング言語文に基づいて制御フローグラフを生成し、第２の入力値セットのいずれかが違反しているかどうかを判定するように構成されていてよい。
【０００８】
別の態様では、ソフトウェアシステムを検証する方法が、第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行することと、ソフトウェアシステムの検証を開始すべきソフトウェアシステムの状態を決定することとを含む。例えば、ソフトウェアシステムのシミュレーションは、閉ループシミュレーション技法を用いて実行することができる。方法は、決定された状態においてソフトウェアシステムの検証を開始することと、第２の入力値セットに基づいて、第２のステップセットについてソフトウェアシステムの検証を実行することとを含んでもよい。例えば、ソフトウェアシステムの検証は、有界モデル検査技法を用いて実行されてもよい。さらに、方法は、ソフトウェアシステムの検証の結果を表示ユニットに出力することを含む。また、方法は、ソフトウェアシステムをテストできる複数のテストベクタを生成することを含んでもよい。
【０００９】
さらに、方法は、ソフトウェアシステムにより実行される第１のステップセット中に、ソフトウェアシステムに関連する一連の状態を決定することと、ソフトウェアシステムの各状態に関連する状態変数の値を検証データベースに記憶することとを含んでもよい。
【００１０】
加えて、方法は、ソフトウェアシステムが動作モードで動作し始める状態を一連の状態から瞬時に決定することを含んでもよい。方法は、決定された状態に関連する状態変数の値を用いて、決定された状態においてソフトウェアシステムを初期化することと、初期化されたソフトウェアシステムの検証を決定された状態において開始することとを含んでもよい。
【００１１】
また、方法は、ソフトウェアシステムに関連するプログラミング言語文を解析することと、解析されたプログラミング言語文に基づいて制御フローグラフを生成することと、第２の入力値セットのいずれかが違反しているかどうかを判定することとを含んでもよい。
【００１２】
また別の態様では、非一時的なコンピュータ可読記憶媒体が、機械可読命令を記憶しており、機械可読命令は、処理ユニットにより実行される際に、上述した方法を処理ユニットに実行させるためのものである。
【００１３】
本開示とそれに付随する態様の多くのより完全な理解は、添付の図面に関連して考慮されるときに以下の説明を参照することでより良好に理解されるので、より容易に得られるであろう。
【図面の簡単な説明】
【００１４】
【図１】一実施形態による、ソフトウェアシステムの検証を実行できるデータ処理装置を示すブロック図である。
【図２】一実施形態による、ソフトウェアシステムを検証する例示的な方法を示す処理フローチャートである。
【図３】一実施形態による、ソフトウェアシステムを検証する詳細な方法を示す処理フローチャートである。
【図４】ソフトウェアシステムの検証に適用される手法を示すグラフィック表現である。
【００１５】
様々な実施形態が、図面を参照して記述されており、同様の参照数字が、全体を通して同様の要素を指すために用いられる。以下の説明では、本開示の実施形態の完全な理解をもたらすために、多数の具体的な詳細が示される。これらの具体的な詳細については、本開示の実施形態を実施するために採用する必要がないことは、当業者には明らかであろう。他の例では、周知の材料または方法については、本開示の実施形態を不必要に分かりにくくすることを避けるために、詳細に記述していない。本開示は、様々な修正および代替形態の余地があるが、その具体的な実施形態について、図面に例として示し、本明細書で詳細に記述する。しかし、本開示を開示される具体的な形態に限定する意図はなく、反対に、本開示は、本開示の趣旨および範囲に含まれる全ての修正、等価物、および代替物をカバーするものであることを理解されたい。
【００１６】
一実施形態では、複数の入力値に基づいてソフトウェアシステムを適切な状態において検証するための方法および装置が提供される。典型的に、ソフトウェアシステムは、ハードウェアシステムに関連する１つ以上の機能を実行する役割を担うソフトウェアコンポーネントを含む。ハードウェアシステムは、アダプティブクルーズコントローラを有する車両であってもよい。ソフトウェアシステムは、車両の様々なコンポーネントから速度、前方の車両との距離などの入力を受け取り、入力を処理してコマンドを生成する。コマンドは、車両を加速または減速させるスロットルなどの車両の別のコンポーネントによって処理される。ソフトウェアシステムを集積回路などの埋込みシステムに導入する前に、ソフトウェアシステムの挙動を検証することが重要である。ソフトウェアシステムの誤動作は、アダプティブクルーズコントローラの予期せぬ挙動につながり、場合によっては車両の衝突につながる場合がある。以下の説明では、ソフトウェアシステムの設計および開発中にソフトウェアシステムの検証を実行するための、データ処理システムおよびデータ処理システムによって実行される方法について記述する。
【００１７】
図１は、例えば、本明細書に記述する処理を実行するようにソフトウェアその他によって特に構成されたデータ処理装置としての、実施形態を実装できるデータ処理装置１００のブロック図を示す。データ処理装置１００は、パーソナルコンピュータ、ラップトップコンピュータ、タブレット、スマートフォンなどであってもよい。図１では、データ処理装置１００は、処理ユニット１０２、アクセス可能なメモリ１０４、記憶ユニット１０６、入力ユニット１０８、表示ユニット１１０、およびバス１１２を含む。
【００１８】
処理ユニット１０２は、本明細書で用いる場合、非限定的に、マイクロプロセッサ、マイクロコントローラ、複雑命令セットコンピューティングマイクロプロセッサ、縮小命令セットコンピューティングマイクロプロセッサ、超長命令語マイクロプロセッサ、明示的並列命令コンピューティングマイクロプロセッサ、グラフィックプロセッサ、デジタル信号プロセッサ、またはその他の種類の処理回路など、任意の種類の演算回路を意味する。処理ユニット１０２は、汎用のまたはプログラマブルな論理デバイスまたはアレイ、特定用途向け集積回路、シングルチップコンピュータなどの埋込みコントローラを含んでもよい。
【００１９】
メモリ１０４は、揮発性メモリおよび不揮発性メモリであってよい。メモリ１０４は、処理ユニット１０２と通信のために結合されていてよい。処理ユニット１０２は、メモリ１０４に記憶されている命令および／またはコードを実行可能である。様々なコンピュータ可読記憶媒体が、メモリ１０４に格納され、メモリからアクセスされうる。メモリ１０４は、読出し専用メモリ、ランダムアクセスメモリ、消去可能なプログラマブル読出し専用メモリ、電気的に消去可能なプログラマブル読出し専用メモリ、ハードドライブ、コンパクトディスク、デジタルビデオディスク、ディスケット、磁気テープカートリッジ、メモリカードなどを扱うためのリムーバブルメディアドライブなど、データおよび機械可読命令を記憶するための任意の好適な要素を含んでもよい。
【００２０】
本実施形態では、メモリ１０４は、ＳＤＤ（software design and development）モジュール１１４を含む。
【００２１】
ＳＤＤモジュール１１４は、上述した記憶媒体のいずれかに機械可読命令の形態で記憶されているシミュレーションモジュール１１６および検証モジュール１１８を含み、処理ユニット１０２と通信し、処理ユニットによって実行されてもよい。処理ユニット１０２により実行される際に、ＳＤＤモジュール１１４は、処理ユニット１０２に、ＳＤＤモジュール１１４によって開発されたソフトウェアシステムの検証を実行させ、ソフトウェアシステムをテストできるテストベクタを生成させる。シミュレーションモジュール１１６は、処理ユニット１０２に、第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行させる。ソフトウェアシステムのシミュレーションは、第１のステップセットが第１の入力値セットを用いてソフトウェアシステムにより実行される際に、ソフトウェアシステムに関連する一連の状態を決定することを可能にする。ソフトウェアシステムのシミュレーションは、プラントモデルデータベース１２２によるプラントモデルを用いて実行される。プラントモデルは、ソフトウェアシステムに関連する環境を表現する。
【００２２】
検証モジュール１１８は、処理ユニット１０２に、ソフトウェアシステムの検証を開始すべきソフトウェアシステムの状態を決定させる。検証モジュール１１８は、処理ユニット１０２に、決定された状態においてソフトウェアシステムの検証を開始させ、第２の入力値セットに基づいて、第２のステップセットについてソフトウェアシステムの検証を実行させる。検証モジュール１１８は、処理ユニット１０２に、ソフトウェアシステムの検証の結果を表示ユニット１１０に出力させる。加えて、検証モジュール１１８は、処理ユニット１０２に、ソフトウェアシステムをテストするためのテストベクタを生成させる。上記した機能を実現するために処理ユニット１０２によって実行される方法ステップについては、図２および図３でより詳細に記述していることが分かる。
【００２３】
記憶ユニット１０６は、検証データベース１２０およびプラントモデルデータベース１２２を記憶する非一時的な記憶媒体であってもよい。検証データベース１２０は、ソフトウェアシステムのシミュレーション中に決定された一連の状態に関連する状態変数の値を記憶する。車のアダプティブクルーズコントロール（ＡＣＣ）ソフトウェアシステムでは、状態変数は、ＡＣＣのモード（例えば、スポーツ／エコノミック、速度キープ、距離キープ、渋滞時の低速など）を含んでもよい。「距離キープ」モードでは、ＡＣＣは前方の車両から最小限の距離を維持しなければならない。このモードでの追加の状態変数は、「キープする最小距離」（道路状況、現在の車両の速度、走行モード、車両および乗客の重量によって生じる車両の慣性などによって異なる値を有しうる）、「ＡＣＣの健全状態」（ＡＣＣの適正な機能をクロスチェックする自己診断システムによって設定された値を有しうる）、「次の車両との距離の履歴」（値は、制動を開始した後にセンサから発信され、運転者にとって制動が「スムーズに感じられる」が必要な安全要件が保証されるように、現在の制動状況（例えば、道路、前方の車両の速度変化）に制動力を適応させるために用いられる）である。
【００２４】
入力ユニット１０８は、ソフトウェアシステムを設計、開発、検証、テストするためのユーザコマンドなどの入力信号を受信できる、キーパッド、タッチ検知ディスプレイ、カメラ（ジェスチャに基づく入力を受信するカメラなど）などの入力手段を含んでいてよい。表示ユニット１１０は、ソフトウェアシステムを可視化するグラフィカルユーザインタフェースを、ソフトウェアシステムの検証の結果とともに表示するように構成されていてよい。バス１１２は、処理ユニット１０２、メモリ１０４、記憶ユニット１０６、入力ユニット１０８、および表示ユニット１１０の間の相互接続部として機能する。
【００２５】
当業者であれば、図１に示すハードウェアが、個々の実現形態によって変化しうることを理解するであろう。例えば、光ディスクドライブなどの他の周辺デバイス、ローカルエリアネットワーク（ＬＡＮ）／ワイドエリアネットワーク（ＷＡＮ）／無線（Ｗｉ−Ｆｉなど）アダプタ、グラフィックアダプタ、ディスクコントローラ、入出力（Ｉ／Ｏ）アダプタなども、示したハードウェアに加えてまたはこれらに代えて用いることができる。示した例は、説明のためだけに提供されるものであり、本開示に関するアーキテクチャを限定することを意味するものではない。
【００２６】
本開示の実施形態によるデータ処理装置は、グラフィカルユーザインタフェースを採用するオペレーティングシステムを含む。オペレーティングシステムは、グラフィカルユーザインタフェースに複数の表示ウィンドウを同時に提示することができ、各表示ウィンドウは、異なるアプリケーションまたは同じアプリケーションの異なるインスタンスへのインタフェースを提供する。グラフィカルユーザインタフェース内のカーソルは、ポインティングデバイスを用いてユーザによって操作されてもよい。望ましい応答を引き起こすために、カーソルの位置を変更したり、マウスボタンをクリックするなどのイベントを発生させたりしてもよい。
【００２７】
市販されている様々なオペレーティングシステムの１つ、例えば、Ｍｉｃｒｏｓｏｆｔ  Ｃｏｒｐｏｒａｔｉｏｎ（Ｒｅｄｍｏｎｄ，Ｗａｓｈｉｎｇｔｏｎ）の製品であるＭｉｃｒｏｓｏｆｔ  Ｗｉｎｄｏｗｓ（商標）バージョンなどが、適切に修正されていれば、採用されてもよい。オペレーティングシステムは、記述するような本開示に従って修正または作成される。
【００２８】
開示している実施形態は、統合された開発環境においてソフトウェアシステムを検証するシステムおよび方法を提供する。特に、開示している技術は、ソフトウェアシステムのシミュレーションを実行し、検証を開始すべきソフトウェアシステムに関連する状態を決定し、決定された状態におけるソフトウェアシステムの検証を開始し、ソフトウェアシステムの検証を実行し、ソフトウェアシステムの検証の結果を表示ユニットに出力することができる。
【００２９】
当業者であれば、簡略化および明確化のために、本開示での使用に適した全てのデータ処理装置の完全な構造および動作が、本明細書に示されたり、記述されたりしていないことを認識するであろう。代わりに、本開示に固有の、または本開示の理解に必要な、データ処理装置の一部のみが示され、記述されている。データ処理装置１００の構成および動作の残りの部分は、当該技術分野で知られている現在の様々な実現形態および実践形態のいずれかに準拠していてよい。
【００３０】
図２は、一実施形態による、ソフトウェアシステムを検証する例示的な方法を示す処理フローチャート２００である。行為２０２では、ソフトウェアシステムのシミュレーションが、第１の入力値セットに基づいて、第１のステップセットについて実行される。例えば、ソフトウェアシステムのシミュレーションは、閉ループシミュレーション技法を用いて実行される。閉ループシミュレーション技法では、ソフトウェアシステムの環境を表現するプラントモデルを用いて、ソフトウェアシステムのシミュレーションが行われる。ソフトウェアシステムのシミュレーションは、ソフトウェアシステムの初期化モード中に第１のステップセットについて実行される。ソフトウェアシステムのシミュレーションは、ソフトウェアシステムを、ソフトウェアシステムの検証を実行できる望ましい状態にするのに役立つ。例えば、ソフトウェアシステムのシミュレーションは、予め定められた条件を満たすまで実行される。条件は、（ｉ）車のアダプティブクルーズコントロール（ＡＣＣ）システムが開始されて初期化されること、または（ｉｉ）ＡＣＣシステムが「距離キープモード」であり、凍結道路を１０分間走行しており、前方の車が激しく制動し始めたこととすることができる。予め定められた条件に当てはまる場合、プラントモデルによって生成され、ソフトウェアシステムの望ましい状態に導く、入力が決定される。
【００３１】
行為２０４では、ソフトウェアシステムの検証を開始すべき、ソフトウェアシステムの状態が瞬時に決定される。例えば、ソフトウェアシステムは、初期化モードでしばらく動作した後に動作モード（すなわち、望ましい状態）に切り替わってもよい。幾つかの実施形態では、ソフトウェアシステムが動作モードで動作し始める状態が決定される。ソフトウェアシステムが望ましい状態で検証されることが望ましい。代替的には、ソフトウェアシステムが望ましい状態に達した後に、ソフトウェアシステムの挙動が検証されることが望ましい。例えば、車のアダプティブクルーズコントロールの適正な挙動は、凍結道路の状況、車の高い速度、および前方の車との距離が急速に減少していること（例えば、さらに前方の車両との衝突による前方の車の完全停止によると推定される）を検出したときに検証されることになっている。
【００３２】
行為２０６では、ソフトウェアシステムの決定された状態においてソフトウェアシステムの検証が開始される。また、クローズド技法を用いたソフトウェアシステムのシミュレーションが、決定された状態において停止される。検証の開始中に、ソフトウェアシステムのシミュレーション中に得られた状態変数の値を用いて、ソフトウェアシステムは決定された状態において初期化される。行為２０８では、ソフトウェアシステムの検証が、第２の入力値セットに基づいて、第２のステップセットについて実行される。例えば、ソフトウェアシステムの検証は、有界モデル検査技法を用いて実行される。ソフトウェアシステムの検証には、ソフトウェアシステムが仕様に適合しているかどうかの確認、動作モード中のソフトウェアシステムの挙動が期待された挙動を満たしているかどうかの確認などが含まれる。このことは、第２の入力値セットが違反しているかどうかを判定することによって実現される。すなわち、第２の入力値セットに対応する出力値が、期待された出力値と一致する。行為２１０では、ソフトウェアシステムの検証の結果が表示ユニットに出力される。例えば、検証の結果は、違反している１つ以上の入力値を含んでもよい。行為２１２では、望ましい動作モードでソフトウェアシステムをテストできる複数のテストベクタが生成される。
【００３３】
図３は、一実施形態による、ソフトウェアシステムを検証する詳細な方法を示す処理フローチャート３００である。行為３０２では、ソフトウェアシステム上で第１のステップセットが実行される際に、ソフトウェアシステムに関連する一連の状態が決定される。行為３０４では、ソフトウェアシステムの各状態に関連する状態変数の値が検証データベースに記憶される。行為３０６では、ソフトウェアシステムの検証を開始すべきソフトウェアシステムの状態が決定される。幾つかの実施形態では、ソフトウェアシステムが動作モードで動作し始める状態が一連の状態から決定される。プログラム変数の値は、検証の望ましい開始点を反映するように記号的に初期化されると言える。
【００３４】
行為３０８では、決定された状態に関連する状態変数の記憶されている値を用いて、ソフトウェアシステムが決定された状態において初期化される。行為３１０では、初期化されたソフトウェアシステムの検証が、決定された状態において開始される。
【００３５】
行為３１２では、ソフトウェアシステムに関連するプログラミング言語文が解析される。行為３１４では、解析されたプログラミング言語文に基づいて制御フローグラフが生成される。行為３１６では、第２の入力値セットのいずれかが仕様の違反につながるかどうかが判定される。第２の入力値セットが仕様の違反につながると判定された場合、行為３１８では、ソフトウェアシステムの検証が失敗したことを示す通知が、仕様の違反につながった入力値とともに表示ユニットに表示される。第２の入力値セットが仕様の違反につながらないと判定された場合、行為３２０では、ソフトウェアシステムの検証が成功したことを示す通知が表示ユニットに表示される。
【００３６】
図４は、一実施形態による、ソフトウェアシステムの検証に適用される手法を示すグラフィック表現４００である。上で説明したように、１つの入力ポートを有するソフトウェアシステムの検証は、閉ループシミュレーション技法と、それに続く有界モデル検査技法との２つの手法を用いて行われる。まず、プラントモデルによって構成されたソフトウェアシステムのシミュレーションが、閉ループシミュレーション技法を用いて、入力ポートを介して提供される入力値に基づいて、Ｎ個のステップ４０６について実行される。ソフトウェアシステムのシミュレーションにより、ソフトウェアシステムの検証を開始できる一定の状態に達することができる。ソフトウェアシステムのシミュレーション中に、ソフトウェアシステムに関連する一連の状態が決定され、一連の状態に関連する状態変数の値が記憶される。その後、ソフトウェアシステムを検証するための望ましい状態が決定される。したがって、ソフトウェアシステムが、決定された状態に関連する状態変数の値を用いて初期化される。例えば、モータのコントローラは、エンジンを暖めて動作モード（すなわち、望ましい状態）に達するまでに数千サイクルを必要とする場合がある。しかし、エンジンの一定の特性の検証を動作モード中に実行する必要がある場合がある。ソフトウェアシステムのシミュレーションは、望ましい状態（すなわち、エンジンの動作モード）において検証を開始するのに役立つ。別の例では、アダプティブクルーズコントロール（ＡＣＣ）システムが車の運転者によって起動された後、ＡＣＣシステムは、ＡＣＣシステムが車の制動システムを制御できるよう、車のモニタリング状態を初期化するための数百サイクルを必要とする。
【００３７】
この場合、ソフトウェアシステムの検証が、有界モデル検査技法を用いて、複数の入力値に基づいて、Ｍ個のステップ４０８について実行される。有界モデル検査技法により、Ｍ個のステップ４０８についてソフトウェアシステムの挙動を網羅的に探索することができる。例示的な一実現形態では、Ｃレベルモデルチェッカが、プログラミング言語文（例えば、Ｃ言語文）を処理し、プログラミング言語文を記号表現（例えば、制御フローグラフ）に変換する。Ｃレベルモデルチェッカは、違反（ソフトウェアシステムの異常挙動）につながる１つ以上の入力値を決定する。このことは、制御フローグラフをスキャンして、制御フローグラフ内の違反につながるパスを特定することによって実現される。例えば、Ｃモデルチェッカは、制御フローグラフをスキャンし、違反につながるパスを特定するために、決定手続を用いる。決定手続は、ブーリアンとして表現されるパスの到達可能性を解くために、非線形演算および配列を含むビットベクトル論理を採用してもよい。
【００３８】
グラフィック表現４００は、ソフトウェアシステムの検証に用いる手法を示している。グラフィック表現４００は、ソフトウェアシステムの検証中にソフトウェアシステム上で実行されるステップを表現するＸ軸４０４と、ソフトウェアシステムのシミュレーションおよび検証に用いる入力の数を表現するＹ軸４０２とを含む。グラフィック表現４００に示すように、ソフトウェアシステムのシミュレーションは、Ｎ個のステップ４０６のそれぞれで受け取った単一の入力値に基づいて、Ｎ個のステップ４０６について実行される。したがって、グラフィック表現４００は、シミュレーションによってカバーされる入力空間の形状を曲線４１０として示している。ソフトウェアシステムのシミュレーションに続いて、ソフトウェアシステムの検証は、Ｎ個のステップ４０６のそれぞれで受け取った複数の入力値に基づいて、望ましい状態においてＭ個のステップ４０８について実行される。したがって、有界モデル検査技法によってカバーされる入力空間４１２の形状が、１つの領域となる。
【００３９】
様々な実施形態では、図１から図４に記載した方法および装置は、閉ループシミュレーションと有界モデル検査との組み合わせを用いてソフトウェアシステムを検証する。これは、ソフトウェアシステムの初期化中、ソフトウェアシステムのシミュレーションが多くのステップについて実行され、ただし、可能な入力空間の小さな部分をカバーするためである。有利には、ソフトウェアシステムのシミュレーションが、ソフトウェアシステムをその検証のための望ましい状態に素早く至らしめる。また、ステップ数の観点におけるカバー率を高めることが実現される。ソフトウェアシステムの望ましい状態（動作モード）では、有界モデル検査が、少数のステップではあるが、広い入力空間について実行される。それゆえ、大きな入力空間にわたって、より多くの誤った入力値を検出する可能性がより高くなる。また、検証の深さも増すことになる。
【００４０】
本明細書に記述したシステムおよび方法は、様々な形態のハードウェア、ソフトウェア、ファームウェア、専用プロセッサ、またはそれらの組み合わせで実装されうることを理解されたい。本実施形態の１つ以上は、１つ以上のコンピュータ、プロセッサ、もしくは命令実行システムによってまたはそれらに関連して用いるためのプログラムコードを記憶しているコンピュータ使用可能媒体またはコンピュータ可読媒体からアクセス可能なプログラムモジュールを含む、コンピュータプログラム製品の形態をとってもよい。本説明のために、コンピュータ使用可能媒体またはコンピュータ可読媒体は、命令実行システム、装置、もしくはデバイスによってまたはそれらに関連して用いるためのプログラムを含み、記憶し、通信し、伝送し、または伝達できる任意の装置とすることができる。媒体は、電子的、磁気的、光学的、電磁的、赤外線式、もしくは半導体のシステム（もしくは装置もしくはデバイス）とすることができ、または、信号キャリアが、半導体もしくはソリッドステートメモリ、磁気テープ、リムーバブルコンピュータディスケット、ランダムアクセスメモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、硬質磁気ディスク、ならびにコンパクトディスク読出し専用メモリ（ＣＤ−ＲＯＭ）、コンパクトディスク読出し／書込み、およびデジタルバーサタイルディスク（ＤＶＤ）などの光ディスクなどを含む物理的なコンピュータ可読媒体の定義に含まれない場合には、伝送媒体（その内部もしくはそれ自体）とすることができる。本技術の各態様を実装するためのプロセッサおよびプログラムコードの両方は、当業者に知られているように集中型または分散型（またはそれらの組み合わせ）とすることができる。
【００４１】
本開示について幾つかの実施形態を参照して詳細に記述してきたが、本開示がそれらの実施形態に限定されないことを理解されたい。本開示を考慮すれば、本明細書に記述するような本開示の様々な実施形態の範囲から逸脱しない、多くの修正および変形が、当業者には想起されるであろう。したがって、本開示の範囲は、前述した説明ではなく、以下の請求項によって示される。請求項の意味および等価物の範囲内に入る全ての変更、修正、および変形は、それらの範囲内で考慮される。
【図１】
2022502774.tif 000003
【図２】
2022502774.tif 000004
【図３】
2022502774.tif 000005
【図４】
2022502774.tif 000006
【手続補正書】
【提出日】令和2年7月8日(2020.7.8)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
ソフトウェアシステムを検証するためのデータ処理装置（１００）であって、該データ処理装置（１００）が、
少なくとも１つの処理ユニット（１０２）と、
前記処理ユニット（１０２）に通信可能に結合された少なくとも１つのメモリユニット（１０４）と、
を備え、
前記メモリユニット（１０４）が、
第１の入力値セットに基づいて、第１のステップセットについて前記ソフトウェアシステムのシミュレーションを実行するように構成されたシミュレーションモジュール（１１６）と、
検証モジュール（１１８）であって、
前記ソフトウェアシステムの検証を開始すべき前記ソフトウェアシステムの状態を決定し、
決定された前記状態において前記ソフトウェアシステムの検証を開始し、
第２の入力値セットに基づいて、第２のステップセットについて前記ソフトウェアシステムの検証を実行し、
前記ソフトウェアシステムの前記検証の結果を表示ユニット（１１０）に出力する
ように構成された、検証モジュール（１１８）と、
を備え、
前記検証モジュール（１１８）が、
前記ソフトウェアシステムに関連するプログラミング言語文を解析し、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成し、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定する
ようにさらに構成されている、
データ処理装置（１００）。
【請求項２】
前記検証モジュール（１１８）が、前記ソフトウェアシステムをテストするための複数のテストベクタを生成するように構成されている、請求項１記載のデータ処理装置（１００）。
【請求項３】
前記シミュレーションモジュール（１１６）が、閉ループシミュレーション技法を用いて前記ソフトウェアシステムの前記シミュレーションを実行するように構成されている、請求項１または２記載のデータ処理装置（１００）。
【請求項４】
前記検証モジュール（１１８）が、有界モデル検査技法を用いて前記ソフトウェアシステムの前記検証を実行するように構成されている、請求項１または２記載のデータ処理装置（１００）。
【請求項５】
前記シミュレーションモジュール（１１６）が、
前記ソフトウェアシステムにより実行される前記第１のステップセット中に、前記ソフトウェアシステムに関連する一連の状態を決定し、
前記ソフトウェアシステムの各状態に関連する状態変数の値を検証データベースに記憶する
ように構成されている、請求項１から４までのいずれか１項記載のデータ処理装置（１００）。
【請求項６】
前記検証モジュール（１１８）は、
前記ソフトウェアシステムが動作モードで動作し始める状態を前記一連の状態から瞬時に決定する
ように構成されている、請求項１から５までのいずれか１項記載のデータ処理装置（１００）。
【請求項７】
前記検証モジュール（１１８）が、
決定された前記状態に関連する前記状態変数の値を用いて、決定された前記状態において前記ソフトウェアシステムを初期化し、
初期化された前記ソフトウェアシステムの検証を決定された前記状態において開始する
ように構成されている、請求項１から６までのいずれか１項記載のデータ処理装置（１００）。
【請求項８】
ソフトウェアシステムを検証する方法であって、該方法が、
データ処理装置（１００）により、第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行することと、
前記データ処理装置（１００）により、前記ソフトウェアシステムの検証を開始すべき前記ソフトウェアシステムの状態を決定することと、
前記データ処理装置（１００）により、決定された前記状態において前記ソフトウェアシステムの検証を開始することと、
前記データ処理装置（１００）により、第２の入力値セットに基づいて、第２のステップセットについて前記ソフトウェアシステムの検証を実行することと、
前記データ処理装置（１００）により、前記ソフトウェアシステムの前記検証の結果を表示ユニット（１１０）に出力することと、
を含み、
前記ソフトウェアシステムの前記検証を実行することが、
前記ソフトウェアシステムに関連するプログラミング言語文を解析することと、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成することと、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定することと
を含む、
方法。
【請求項９】
前記方法が、前記データ処理装置（１００）により、前記ソフトウェアシステムをテストできる複数のテストベクタを生成することをさらに含む、請求項８記載の方法。
【請求項１０】
前記ソフトウェアシステムの前記シミュレーションが、閉ループシミュレーション技法を用いて実行される、請求項８または９記載の方法。
【請求項１１】
前記ソフトウェアシステムの前記検証が、有界モデル検査技法を用いて実行される、請求項８または９記載の方法。
【請求項１２】
前記ソフトウェアシステムの前記シミュレーションを実行することが、
前記ソフトウェアシステムにより実行される前記第１のステップセット中に、前記ソフトウェアシステムに関連する一連の状態を決定することと、
前記ソフトウェアシステムの各状態に関連する状態変数の値を検証データベース（１２０）に記憶することと
を含む、請求項８から１１までのいずれか１項記載の方法。
【請求項１３】
前記ソフトウェアシステムの前記検証を開始すべき前記ソフトウェアシステムの前記状態を決定することが、
前記ソフトウェアシステムが動作モードで動作し始める状態を前記一連の状態から決定すること
を含む、請求項８から１２までのいずれか１項記載の方法。
【請求項１４】
決定された前記状態において前記ソフトウェアシステムの前記検証を開始することが、
決定された前記状態に関連する前記状態変数の値を用いて、決定された前記状態において前記ソフトウェアシステムを初期化することと、
初期化された前記ソフトウェアシステムの検証を決定された前記状態において開始することと
を含む、請求項８から１３までのいずれか１項記載の方法。
【請求項１５】
非一時的なコンピュータ可読記憶媒体であって、機械可読命令を記憶しており、前記機械可読命令は、処理ユニット（１０２）により実行される際に、前記処理ユニット（１０２）に、
第１の入力値セットに基づいて、第１のステップセットについてソフトウェアシステムのシミュレーションを実行することと、
前記ソフトウェアシステムの検証を開始すべき前記ソフトウェアシステムの状態を決定することと、
決定された前記状態において前記ソフトウェアシステムの検証を開始することと、
第２の入力値セットに基づいて、第２のステップセットについて前記ソフトウェアシステムの検証を実行することと、
前記ソフトウェアシステムの前記検証の結果を表示ユニットに出力することと
を含む方法を実行させるためのものであり、
前記ソフトウェアシステムの前記検証を実行することが、
前記ソフトウェアシステムに関連するプログラミング言語文を解析することと、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成することと、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定することと
を含む、
記憶媒体。
【請求項１６】
前記機械可読命令は、前記処理ユニット（１０２）に、
前記ソフトウェアシステムをテストできる複数のテストベクタを生成すること
を含む方法ステップを実行させるためのものである、請求項１５記載の記憶媒体。
【請求項１７】
前記機械可読命令は、前記処理ユニット（１０２）に、
前記ソフトウェアシステムに関連するプログラミング言語文を解析することと、
解析された前記プログラミング言語文に基づいて制御フローグラフを生成することと、
前記第２の入力値セットのいずれかが前記ソフトウェアシステムの仕様の違反につながるかどうかを判定することと
を含む方法ステップを実行させるためのものである、請求項１５または１６記載の記憶媒体。
【請求項１８】
前記ソフトウェアシステムの前記シミュレーションが、閉ループシミュレーション技法を用いて実行され、前記ソフトウェアシステムの前記検証が、有界モデル検査技法を用いて実行される、請求項１５から１７までのいずれか１項記載の記憶媒体。
【国際調査報告】
2022502774.tif 000007
2022502774.tif 000008
2022502774.tif 000009