JP6976064B2 - モデルチェックのためのデータ構造抽象化 - Google Patents

Description

優先権主張
本発明は、２０１６年３月９日に出願されたインド非仮出願（名称：DATA STRUCTURE ABSTRACTION FOR MODEL CHECKING）第２０１６２１００８２８４号の優先権を主張するものである。上記出願の内容全体は、参照により本明細書に援用される。

本開示は、概して、データ構造抽象化に関し、より詳細には、モデルチェックのためにデータ構造を抽象化する方法及びシステムに関する。

ソフトウェアプログラムとも呼ばれるコンピュータプログラムは、コンピュータプログラムが実行されるコンピューティングデバイスで特定のタスクを実行する、プログラミング言語で書かれたコードを含む。コンピューティングデバイスの例としては、ラップトップ、個人情報端末（ＰＤＡ）、コンピュータ、モバイル電話等が挙げられるが、これらに限定されない。コードの検証は、ソフトウェアプログラムの安全な実行に最もに重要なものである。例えば、全ての種類のソフトウェアプログラムで欠陥検出を実行することは必須である。

静的分析が、サウンド欠陥検出に一般に使用される技法である。静的分析は、静的検証器が任意の所与の入力での欠陥検出を実行して、それにより、プログラムの正確性を論証することによる検証を含む。ソフトウェアプログラムを検証する別の技法は、モデルチェックを含む。モデルチェックは、モデルチェッカーによるプログラムの正確性の検証を含む。モデルチェックは、スカラーを含むプログラムの属性を効率的にチェックするのに利用することができる。

本発明者らはここで、以下に説明するように、欠陥検出又はプログラム検証のそのような従来のシステムに伴う幾つかの技術的問題を認識した。静的分析により実行される検証はスケーラブルであるが、コードの検証には不正確であることが観測されている。モデルチェックの技法は、スカラーを含むプログラムの属性チェックに有効であるが、アレイ及びC式構造等のデータ構造を含むプログラムをモデルチェックする間、プログラムは、ステート空間爆発に陥ることが多い。現実のプログラムはそのようなデータ構造でいっぱいであるため、モデルチェックはそのようなプログラムには有効ではない。

本開示の実施形態は、従来のシステムにおいて本発明者らが認識した上記技術的問題の１つ又は複数への解決策としての技術改善を提示する。例えば、一実施形態では、モデルチェックのためにデータ構造を抽象化するプロセッサにより実施される方法が提供される。本方法は、１つ又は複数のハードウェアプロセッサを介して、抽象化するソースコードを受信することを含む。更に、本方法は、１つ又は複数のハードウェアプロセッサを介して、ソースコード内の１つ又は複数のデータ構造アクセスを識別することを含み、１つ又は複数のデータ構造アクセスは、ソースコード内のデータ構造にアクセスするために、データ構造の要素を参照する表現を含む。更に、本方法は、１つ又は複数のハードウェアプロセッサを介して、１つ又は複数のデータ構造アクセスでの１つ又は複数のループを識別することを含む。１つ又は複数のループのうちのループは、制御ステートメント及びループ本体を含み、ループは、ループ本体を制御ステートメントに基づいて繰り返し実行させる。更に、本方法は、１つ又は複数のハードウェアプロセッサを介して、１つ又は複数のループ内の１つ又は複数のループタイプを識別することを含む。また、本方法は、１つ又は複数のハードウェアプロセッサを介して、１つ又は複数のループタイプに基づいて抽象化コードを生成することを含み、抽象化コードは、データ構造を抽象化することが可能であり、データ構造を抽象化することは、１つ又は複数のループの各ループについて、データ構造のアクセスされる要素に基づいて、１つ又は複数のデータ構造アクセスを前記ループのループ本体内の対応する代表的な要素及び非決定論的値のうちの一方で置換すること、前記ループのループタイプに基づいて、データ構造の要素に作用する前記ループのループ制御ステートメントをなくすこと、及びループ本体の冒頭及びソースコードのループ本体の後に、複数の非アレイ割り当てを追加することを実行することを含む。また、本方法は、１つ又は複数のハードウェアプロセッサを介して、モデルチェックのために抽象化コードを提供することを含む。

別の実施形態では、モデルチェックのためにデータ構造を抽象化するシステムが提供される。本システムは、少なくとも１つのメモリと、１つ又は複数のハードウェアプロセッサとを含み、少なくとも１つのメモリは１つ又は複数のハードウェアプロセッサに接続され、１つ又は複数のハードウェアプロセッサは、少なくとも１つのメモリに記憶されたプログラム命令を実行して、抽象化するソースコードを受信することが可能である。更に、１つ又は複数のハードウェアプロセッサは、ソースコード内の１つ又は複数のデータ構造アクセスを識別するプログラム命令を実行することが可能であり、１つ又は複数のデータ構造アクセスは、ソースコード内のデータ構造にアクセスするために、データ構造の要素を参照する表現を含む。更に、１つ又は複数のハードウェアプロセッサは、１つ又は複数のデータ構造アクセスでの１つ又は複数のループを識別するプログラム命令を実行することが可能である。１つ又は複数のループのうちのループは、制御ステートメント及びループ本体を含み、ループは、ループ本体を制御ステートメントに基づいて繰り返し実行させる。更に、１つ又は複数のハードウェアプロセッサは、１つ又は複数のループ内の１つ又は複数のループタイプを識別するプログラム命令を実行することが可能である。また、１つ又は複数のハードウェアプロセッサは、１つ又は複数のループタイプに基づいて抽象化コードを生成するプログラム命令を実行することが可能であり、抽象化コードは、データ構造を抽象化することが可能であり、データ構造を抽象化することは、１つ又は複数のループの各ループについて、データ構造のアクセスされる要素に基づいて、１つ又は複数のデータ構造アクセスを前記ループのループ本体内の対応する代表的な要素及び非決定論的値のうちの一方で置換すること、前記ループのループタイプに基づいて、データ構造の要素に作用する前記ループのループ制御ステートメントをなくすこと、及びループ本体の冒頭及びソースコードのループ本体の後に、複数の非アレイ割り当てを追加することを実行することを含む。また、１つ又は複数のハードウェアプロセッサは、モデルチェックのために抽象化コードを提供するプログラム命令を実行することが可能である。

更に別の実施形態では、非一時的コンピュータ可読媒体であって、モデルチェックのためのデータ構造抽象化の方法を実行するコンピュータプログラムをその上で具現した非一時的コンピュータ可読媒体が提供される。方法は、抽象化するソースコードを受信することを含む。更に、方法は、ソースコード内の１つ又は複数のデータ構造アクセスを識別することを含み、１つ又は複数のデータ構造アクセスは、ソースコード内のデータ構造にアクセスするために、データ構造の要素を参照する表現を含む。更に、方法は、１つ又は複数のデータ構造アクセスでの１つ又は複数のループを識別することを含む。１つ又は複数のループのうちのループは、制御ステートメント及びループ本体を含み、ループは、ループ本体を制御ステートメントに基づいて繰り返し実行させる。更に、方法は、１つ又は複数のループ内の１つ又は複数のループタイプを識別することを含む。また、方法は、１つ又は複数のループタイプに基づいて抽象化コードを生成することを含み、抽象化コードは、データ構造を抽象化することが可能であり、データ構造を抽象化することは、１つ又は複数のループの各ループについて、データ構造のアクセスされる要素に基づいて、前記ループのループ本体内の対応する代表的な要素及び非決定論的値のうちの一方で１つ又は複数のデータ構造アクセスを置換すること、前記ループのループタイプに基づいて、データ構造の要素に作用する前記ループのループ制御ステートメントをなくすこと、及びループ本体の冒頭及びソースコードのループ本体の後に、複数の非アレイ割り当てを追加することを実行することを含む。また、方法は、モデルチェックのために抽象化コードを提供することを含む。

上記概説及び以下の詳細な説明が、単なる例示及び説明のためのものであり、特許請求の範囲に記載されるような本発明の限定ではないことを理解されたい。

本開示に組み込まれ、本開示の一部をなす添付図面は、例示的な実施形態を示し、説明と一緒に、開示される原理を説明する役割を果たす。

本開示の幾つかの実施形態による、データ構造を抽象化するシステムのブロック図を示す。 本開示の幾つかの実施形態による、データ構造を抽象化する方法の流れ図である。

例示的な実施形態について添付図面を参照して説明する。図中、参照番号の一番左の１つ又は複数の桁は、参照番号が最初に現れる図を示す。好都合な場合は常に、同じ参照番号が、図面全体を通して同じ又は同様の部分を指すために使用される。開示される原理の例及び特徴が本明細書に記載されるが、変更形態、適合形態、及び他の実装形態が、開示される実施形態の趣旨及び範囲から逸脱せずに可能である。以下の詳細な説明が、単なる例示としてみなされ、真の範囲及び趣旨が以下の特許請求の範囲により示されることが意図される。

ソフトウェアコードでは、データ構造演算は、一般にループ内で行われる。本明細書では、データ構造は、データの有効使用を可能にするようにコンピュータ内でデータを編成する方法を指し得る。データ構造を有するプログラム（又はソフトウェアコード）の実行中、データ構造のサイズに応じて、無限ループ又は大きいループ境界を有するループの場合、エラーに直面し得る。本明細書では、ループ境界は、ループを実行する必要がある最大回数として理解し得る。一般に、プログラムのエラーのない実行を保証するために、プログラムはまず、例えば、コンピュータデバイスのプログラム解析器又はモデルチェッカーによりエラーについてチェックされる。モデルチェッカーは、プログラムを分析し、プログラムの実行時に生じ得る様々なエラーについてチェックするように構成される。しかし、非決定論的境界を有するループの場合、すなわち、無限又は大きいループ境界の場合、モデルチェッカーは、小さい上限を確定し、上限に従ってループを展開する。更に上限の確定は、モデルチェッカーがそのような境界を確定するのに十分なインテリジェンスを欠き得るため、モデルチェッカーにとって時間がかかり困難なタスクであり得る。したがって、不適切な、すなわち、必要とされるよりも小さい境界を提供することは、有界モデルチェッカーにループ展開アサーション失敗等の結果を生成させ得る。更に、境界がより小さい場合及び境界がより大きい場合の両方で、モデルチェッカーは「メモリ不足」失敗を生じさせ得る。したがって、有界モデルチェッカーを使用して無限又は大きい境界を有するループを検証することは実現可能ではないことがある。

本主題の実装形態によれば、ソースコードのモデルチェックのためにソースコード内のデータ構造を抽象化するシステム及び方法が記載される。ソースコードは、プログラミング言語で書かれたコンピュータプログラムとして理解し得る。システム及び方法は、様々なコンピューティングデバイスで実施することができる。コンピューティングデバイスは、デスクトップコンピュータ、ハンドヘルドデバイス、ラップトップ、又は他のポータブルコンピュータ等を含むが、これらに限定されない。一実装形態では、データ構造抽象化を実施するシステム及び方法は、C、C++、VC++、C#等を含むが、これらに限定されないプログラミング言語を使用して書かれたプログラムでのデータ構造抽象化及び続くモデルチェックに提供し得る。

一実装形態では、抽象化のために受信されるソースコードを分析して、ループ本体と、制御ステートメントとを有するループ内のデータ構造アクセスを特定し得る。更に、非データ構造変数を意味する他の変数が、ループ内で識別される。更に、元のプログラムに対応する抽象プログラムを生成し得る。本明細書では、抽象化のために受信されるソースコードは、理解を容易にするため、及び受信コード（元のプログラム）を抽象プログラム／コードと区別するために、元のプログラムと呼ばれる。元のコードに対応する抽象プログラムを生成するために、ソースコード内の全てのデータ構造アクセスは、代表的な要素で置換される。本明細書では、代表的な要素は、データ構造の任意の要素であり得、それにより、代表的な要素が、データ構造の他の要素と同じフォーマット及び属性を有し得ることを暗黙的に示す。更に、ループ制御ステートメントは、非決定論的選択のifステートメントで置換し得る。更に、全ての非データ構造変数への非決定論的割り当てが、ループ本体の冒頭及びループ本体の後に追加される。方法は更に、モデルチェックのための抽象プログラムを生成する。

本明細書では、ループ内のループ制御ステートメントは、データ構造の反復条件として理解し得る。ループは、完全ループ及び部分ループとして分類することができる。完全ループは、データ構造の全ての要素がアクセスされるような複数の条件を含む。部分ループでは、データ構造要素のサブセットがアクセス又は反復する。部分ループは、ループ内で条件ブレークステートメント若しくは継続ステートメントを使用すること、又は１以外の整数でループを増分／減分することを含むが、これらに限定されない様々な方法で実施することができる。

一実装形態では、Cプログラム等のコンピュータプログラムでのループ内のデータ構造アクセスは抽象化される。コンピュータプログラム内のデータ構造を抽象化するために、「ａ」と呼ばれるデータ構造で検証すべき各属性を特定することができ、アサーションとしてモデリングし得る。更に、コンピュータプログラムは、属性「ａ」に関してスライスされ、低減されたスライスコンピュータプログラムが属性「ａ」の検証に使用される。データ構造アクセスを有するループは除去され、データ構造アクセスは抽象化される。次に、抽象化コンピュータプログラムは、モデルチェッカーを使用して分析される。モデルチェッカーが、抽象化コンピュータプログラムの属性「ａ」を安全として報告する場合、属性「ａ」が、元のコンピュータプログラムで安全であると安全に結論付けることができる。

更に、本データ抽象方法は、データ構造アクセスがループ内にある場合、ループヘッダを適切な「if条件」で置換し、データ構造アクセスがループ本体外にある場合、「if条件」を導入する。また、コンピュータプログラム入れ子ループが、最も内側のループ本体から開始して、コンピュータプログラムの最も外側のループ本体に進んで抽象化される。更に、データ構造アクセスがループ内にある場合、各非データ構造変数は、非決定論的値を抽象ループの冒頭及びループ本体の後にそれに割り当てることにより抽象化される。

したがって、本主題のシステム及び方法は、プログラムでデータ構造抽象化プロセスを実施することに役立つ。元のプログラムは、アレイ及びループのない抽象化プログラム／コードとも呼ばれる別のプログラムで置換される。これにより、メモリリソース、処理リソース、並びに違法ポインタの逆参照等の時間消費及びエラーの使用を低減した状態で、プログラムが実行されることが保証される。更に、コンピュータプログラムは、追加の実行と共に元のコンピュータプログラムの全ての実行が可能な別のコンピュータプログラムに抽象化し得る。そのような抽象化コンピュータプログラムは、元のコンピュータプログラムの過剰近似と呼ばれ得る。したがって、コンピュータプログラムの属性が、抽象化コンピュータプログラムで有効である場合、これは元のコンピュータプログラムでも当てはまる。更に、データ構造抽象化プロセスを適用した後、アサーションがコンピュータプログラムで安全である場合、モデルチェッカーは、アサーションが安全であることを返し、その場合、元のコンピュータプログラムはそのアサーションに関して安全である。

本主題のこれら及び他の利点は、以下の図と併せて更に詳細に説明される。説明されるプログラムのデータ構造を抽象化するシステム及び方法の態様は、様々なコンピューティングシステム、環境、及び／又は構成で実施することができるが、実装形態は以下の例示的なシステムに関連して説明される。

図１は、本主題の実装形態による、プログラミング言語で書かれたプログラムでデータ構造抽象化を実施するデータ構造抽象化システム１００のブロック図を示す。データ構造抽象化システム１００は、コンピューティングデバイスで実施し得る。コンピューティングデバイスの例としては、メインフレームコンピュータ、ワークステーション、パーソナルコンピュータ、デスクトップコンピュータ、ミニコンピュータ、サーバ、マルチプロセッサシステム、ラップトップ、個人情報端末、スマートフォン、及びモバイル電話等のセルラ通信デバイス等が挙げられるが、これらに限定されない。コンピューティングデバイスを使用して実施されるデータ構造抽象化システム１００は、１つ又は複数のプロセッサ１０２、ＩＯインタフェース１０４、及びプロセッサ１０２に接続されたメモリ１０６を含む。プロセッサ１０２は、単一の処理ユニット又は幾つかのユニットであることができる。プロセッサ１０２は、１つ又は複数のマイクロプロセッサ、マイクロコンピュータ、マイクロコントローラ、デジタル信号プロセッサ、中央演算処理装置、状態機械、論理回路、及び／又は演算命令に基づいて信号を操作する任意のデバイスとして実施し得る。他の機能の中でも特に、プロセッサ１０２は、メモリ１０６に記憶されたコンピュータ可読命令及びデータをフェッチし実行するように構成される。

「プロセッサ」と記される任意の機能ブロックを含め、図に示される様々な要素の機能は、適切なソフトウェアに関連してソフトウェアを実行することができる専用ハードウェア及びハードウェアの使用を通して提供し得る。プロセッサにより提供される場合、機能は、単一の専用プロセッサ、単一の共有プロセッサ、又は幾つかを共有し得る複数の個々のプロセッサにより提供し得る。更に、「プロセッサ」という用語の明示的な使用は、ソフトウェアを実行可能なハードウェアを排他的に指すものとして解釈されるべきではなく、限定ではなく、デジタル信号プロセッサ（ＤＳＰ）ハードウェア、ネットワークプロセッサ、特定用途向け集積回路（ＡＳＩＣ）、フィールドプログラマブルゲートアレイ（ＦＰＧＡ）、ソフトウェアを記憶する読み取り専用メモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、及び不揮発性記憶装置を暗黙的に含み得る。従来の及び／又はカスタマイズされた他のハードウェアを含むこともできる。

ＩＯインタフェース１０４は、様々なソフトウェアインタフェース及びハードウェアインタフェース、例えば、キーボード、マウス、外部メモリ、及びプリンタ等の周辺機器のインタフェースを含み得る。更に、ＩＯインタフェース１０４は、コンピューティングデバイスが、パーソナルコンピュータ、ラップトップ等の他のコンピューティングデバイスと通信できるようにし得る。

メモリ１０６は、例えば、スタティックランダムアクセスメモリ（ＳＲＡＭ）及びダイナミックランダムアクセスメモリ（ＤＲＡＭ）等の揮発性メモリ及び／又は読み取り専用メモリ（ＲＯＭ）、消去可能プログラマブルＲＯＭ、フラッシュメモリ、ハードディスク、光ディスク、及び磁気テープ等の不揮発性メモリを含む当技術分野で既知の任意のコンピュータ可読媒体を含み得る。メモリ１０６は、モジュール１０８及びデータ１１０を含むこともできる。

モジュール１０８は、特定のタスクを実行するか、又は特定の抽象データ型を実施するルーチン、プログラム、オブジェクト、コンポーネント、データ構造等を含む。モジュール１０８は、データ構造抽象化モジュール、モデルチェッカーモジュール、及び他のモジュールを更に含む。他のモジュールは、コンピューティングデバイスのアプリケーション及び機能を補足するプログラム又は符号化命令を含み得る。

データ１１０は、特に、モジュール１０８の１つ又は複数により処理、受信、及び生成されたデータを記憶するリポジトリとして機能する。データ１１０は、例えば、抽象化データ及び他のデータを含む。他のデータは、他のモジュールの１つ又は複数のモジュールが実行された結果として生成されるデータを含む。

実施形態では、コンピューティングデバイスは、抽象化するソースコードを受信し得る。ソースコードは、プログラム又はソフトウェアプログラムと呼ばれ得る。実施形態では、コンピューティングデバイスは、コンパイルモジュールからソースコードを受信し得る。様々な実施形態では、コンパイルモジュールは、コンピューティングデバイスの内部にあってもよく、又は外部にあってもよい。

ソースコードを受信すると、システム１００は、ソースコード内の１つ又は複数のデータ構造アクセスを識別するようにされ得る。データ構造アクセスは、ソースコード内のデータ構造にアクセスするデータ構造の要素を参照する表現を含む。データ構造アクセスの例は、アレイ、ハッシュテーブル、グラフ、ツリー、クラス、セット、及びマップを含み得るが、これらに限定されない。

システム１００は更に、１つ又は複数のデータ構造アクセス内の１つ又は複数のループを識別するようにされ得る。１つ又は複数のループのうちのループは、制御ステートメント及びループ本体を含み、それにより、ループは、ループ本体を制御ステートメントに基づいて繰り返し実行させる。ループステートメントは、通常、特に初期化条件と元のループの終了条件とを含み得る。

システム１００は更に、１つ又は複数のループ内の１つ又は複数のループタイプを識別するようにされ得る。ループタイプは、完全ループ及び部分ループを含み得る。完全ループは、データ構造の全ての要素にわたり反復するループを含む。部分ループは、データ構造の要素のサブセットにわたり反復するループを含む。

システム１００は更に、１つ又は複数のループタイプに基づいて抽象化コードを生成するようにされ得る。抽象化コードは、データ構造を抽象化することが可能である。実装形態では、システム１００は、ソースコードに存在するデータ構造を抽象化することにより、抽象化コードを生成することが可能である。例えば、前記アレイにわたり反復するアレイ及びループを有するソースコードに対応して、システム１００は、要素数ｎ_ａを有する各アレイａに対応する追加の抽象要素及びインデックス対（ｖ_ａ，ｉ_ａ）を有する変換プログラム（又はソースプログラム）にソースコードを変換するようにされる。実施形態では、ソースコードの抽象化ソースコードへの変換は、非決定論的値を範囲［０．．ｎ_ａ−１］内のｉ_ａに割り当てることにより得られる。

実施形態では、ソースコードの抽象化ソースコードへの変換は、前記ループの１つ又は複数のループタイプに基づいて１つ又は複数のループを変更して、抽象化コードを取得することにより得られる。実施形態では、ループタイプは、完全ループ及び部分ループを含み得る。

完全ループは、データ構造の全ての要素にわたり反復するループを含み、部分ループは、データ構造の要素のサブセットにわたり反復するループを含む。条件１によれば、抽象データ構造を生成するために、システムは、前記ループのループタイプに基づいて、データ構造の要素に作用する前記ループのループ制御ステートメントをなくすことができる。

実施形態では、システムは、前記ループのループタイプが完全ループであると判断することにより、前記ループのループ制御ステートメントをなくすことができる。前記判断がなされると、システム１００は、ループ制御ステートメントをif（真）ステートメントで置換するようにされる。if（真）ステートメントは、if表現、ステートメント、endを含み得、if（真）ステートメントは、表現を評価し、表現が真である場合、ステートメントを実行する。例えば、システムは、for（ｉ＝０；ｉ＜ｎ_ａ；ｉ＋＋）Ｓの形態のループであるａと呼ばれる完全ループをｉ＝ｉ_ａで置換し、Ｖ_ｏ＝＊；Ｓ’；Ｖ_ｏ＝＊は、ループ本体Ｓ内で変更された全ての非アレイ変数への非決定論的値の割り当てである。

別の実施形態では、システムは、前記ループのループタイプが部分ループであると判断することができ、前記判断がなされると、システム１００は、ループ制御ステートメントをif（非決定論的）ステートメントで置換するようにされる。非決定論的関数は、特定の入力値セットと共に呼び出されるときは随時、同じ結果を返し得る。例えば、部分ループは、if（＊）｛Ｖ_ｏ＝＊；Ｓ’｝Ｖ_ｏ＝＊；で置換することができる。

条件２（上述）によれば、抽象データ構造を生成するために、システム１００は、データ構造のアクセスされる要素に基づいて、前記ループのループ本体内の対応する代表要素及び非決定論的値のうちの一方で１つ又は複数のデータ構造アクセスを置換することができる。実施形態では、システム１００はまず、データ構造アクセスの発生ロケーションをソースコードのステートメントの左辺（ＬＨＳ）及び右辺（ＲＨＳ）のうちの一方として判断し得る。

実施形態では、データ構造アクセスの発生ロケーションがソースコードのステートメントのＲＨＳであると判断される場合、システム１００は、前記ループの現在の反復でアクセスされる要素が、前記ループの現在の反復と異なる反復に関連付けられるか否かを判断するようにされ得る。現在の反復でアクセスされる要素が、現在の反復と異なる反復でアクセスされる要素と異なると判断される場合、システム１００は、１つ又は複数のデータ構造アクセスを対応する非決定論的値で置換する。例えば、割り当てのＲＨＳ内の各アレイアクセスａ［ｅ］は、表現ｉ_ａ＝＝ｅ’？ｖ_ａ：＊で置換され、ここで、＊は非決定論的値である。

実施形態では、データ構造アクセスの発生ロケーションがソースコードのステートメントのＬＨＳであると判断される場合、システム１００は、対応する代表的な要素で１つ又は複数のデータ構造アクセスを置換するようにされ得る。例えば、ａ［ｅ］＝ｅ’_１の形態のアレイ要素への各割り当ては、ｅ’＝＝ｉ_ａ？ｖ_ａ＝ｅ’_１；ｅ’_１で置換される。

また、条件３によれば、抽象データ構造を生成するために、システム１００は、ループ本体の冒頭及びソースコードのループ本体の後に、複数の非アレイ割り当てを追加することができる。実施形態では、複数の非アレイ割り当てを追加する前に、システム１００は、ＬＨＳ内のループ本体での非データ構造変数を識別するようにされる。識別すると、システム１００は、ＬＨＳ内のループ本体内非データ構造変数を割り当てるようにされる。

データ構造抽象化の例を以下に提供し、ここで、例１．１は元のソースコードであり、例１．２は、例１．１の元のソースコードに対応する抽象化ソースコードである。

例１．１
例１．１は元の入力ソースコードを含む。

例１．１では、構造のアレイａを有する元のソフトウェアコード（又はプログラム）であり、ここで、ｎｄ（ｌ，ｕ）は、範囲［ｌ：：ｕ］内の非決定論的値を返す。この例では、アレイの全ての要素の各フィールドは、ループ内でゼロに初期化され（１９行目）、次に、別のループで（２５行目）、要素の任意のサブセットに対して、フィールドｑはフィールドｐの二乗に設定される。最後のループ（３２行目）は、各要素で、ｑがｐに等しいか、又はｑがｐ^２に等しいことを表明する。これは線形属性ではなく、したがって、線形不変性を発見する既存の技法又はデータ構造不変性を発見することができない決定可能理論に頼る技法である。有界モデルチェッカーは、そのような不変性の発見に有効であるが、上述したように、有界モデルチェッカーは、大きい境界を有するループを扱うことができない。

例１．１に対応する変換後プログラム（例１．２）が提供される。変換されたコードでは、各アレイアクセスはｘで置換されている。本明細書では、ｘは、アレイａに対応する抽象変数である。アサーション時、ｘの２つの値は

に達する。
元のプログラムでは、アサーションが違反される場合、あるインデックスｉ_０で違反し得、ａ［ｉ_０］の値は、初期化又はａ［ｉ_０］：ｐ及びａ［ｉ_０］：ｑにｋ及びｋ＊ｋがそれぞれ割り当てられるポイントから達することができる。したがって、例えば、属性が元のプログラムで違反の場合、あるｉ_０で違反することになり、ｘが、元のプログラム内でａ［ｉ_０］がとるものと同じ経路をとる抽象プログラムの実行があり、したがって、変換プログラムも属性が違反し得る。この特定の例では、属性が、変換プログラムに対して当てはまらない場合、元のプログラムでも当てはまり得ない。しかし、これは、全ての事例で全体的に当てはまるわけではない。変換コードを以下に示す（例１．２）。

例１．２
例１．２は、例１．１の元の入力ソースコードに対応する抽象化ソースコードを含む。

例１．１のソースコードで見られるように、元のプログラムのコードは、

である。

以下のコードは、データ構造アクセスが完全ループ内にある場合の抽象化（例１．２での）を示す。

例１．１のソースコードで見られるように、元のプログラムのコードは、

である。

以下のコードは、データ構造アクセスが部分ループ内にある場合の抽象化（例１．２での）を示す。

実施形態では、システム１００は、モデルチェックのために抽象化コードを提供するようにされる。条件１、条件２、及び条件３等の条件に基づく抽象化コードの生成を説明する例について、以下の例を参照して説明する。

更に、そうして得られた抽象化データ構造を有するコンピュータプログラムは、プロセッサ１０２により抽象化データに保存し得る。更に、抽象化データ構造を有するプログラムは、モデルチェッカーモジュールに提供されて、エラーについて分析し得る。抽象化データ構造を有するプログラムをモデルチェッカーモジュールに提供することは、抽象データ構造を有する抽象プログラム及び分析のための入力機能の促進に役立ち、コンピュータプログラムの入力アサーション又は属性が安全であるか否かをチェックする。安全である場合、プロセスは停止し、その他の場合、プロセスはトレースを生成する。

本主題は、「whileループ」及び「forループ」を参照して定義されたが、データ構造抽象化を実施するコンピューティングデバイスが、当業者に理解されるような少数の変更形態／代替形態があるが、他のタイプのループでのデータ構造抽象化に使用し得ることが理解される。

本主題は、C言語で書かれたプログラムを参照して定義されたが、データ構造抽象化を実施するコンピューティングデバイスが、少数の変更形態があるが、他のプログラミング言語を使用して書かれたプログラムでのデータ構造抽象化に使用し得ることが理解される。

本主題（例を含む）はアレイを参照して定義されたが、データ構造抽象化を実施するコンピューティングデバイスが、アレイ以外のデータ構造に使用し得ることが理解される。

図２は、実施形態例による、コンピュータプログラムをモデルチェックする、データ構造化を抽象化する例としての方法２００を示す。方法２００では、２０２において、抽象化するソースコード又はコンピュータプログラムを受信し得る。実施形態では、ＩＯ要素１０４は、ソースコードを受信させ得る。２０４において、１つ又は複数のデータアクセスは、プロセッサ１０２等の１つ又は複数のハードウェアプロセッサを介して、ソースコード内で識別される。１つ又は複数のデータ構造アクセスは、ソースコード内のデータ構造にアクセスするために、データ構造の要素を参照する表現を含む。実施形態では、データ構造アクセスは、アレイ、ハッシュテーブル、グラフ、ツリー、クラス、セット、及びマップの１つを含み得る。２０６において、１つ又は複数のループが、プロセッサ１０２等の１つ又は複数のハードウェアプロセッサを介して、１つ又は複数のデータ構造アクセス内で識別される。ループは、制御ステートメント及びループ本体を含み、ループは、制御ステートメントに基づいてループ本体を繰り返し実行させる。

２０８において、１つ又は複数のループタイプが、プロセッサ１０２等の１つ又は複数のハードウェアプロセッサを介して、１つ又は複数のループにおいて識別される。実施形態では、ループタイプは、完全ループ及び部分ループを含む。完全ループ及び部分ループの例は、図１を参照して説明されている。２１０において、抽象化コードが、１つ又は複数のハードウェアプロセッサを介して、１つ又は複数のループタイプに基づいて生成される。抽象化コードは、データ構造を抽象化することが可能である。データ構造の抽象化は、１つ又は複数のループの各ループで、以下の１つを実行することを含む。

データ構造のアクセスされる要素に基づいて、１つ又は複数のデータ構造アクセスを前記ループのループ本体内の対応する代表的な要素及び非決定論的値のうちの一方で置換すること。

実施形態例では、データ構造アクセスの発生ロケーションが特定される。例えば、データ構造の発生ロケーションは、ソースコードのステートメントの左辺（ＬＨＳ）及び右辺（ＲＨＳ）のうちの一方であることができる。実施形態では、データ構造アクセスの発生ロケーションが、ソースコードのステートメントのＲＨＳであると判断される場合、アクセスされる要素に、前記ループの現在の反復と異なる反復が関連付けられているか否かを判断する。アクセスされる要素が前記ループの現在の反復と異なると判断される場合、１つ又は複数のデータ構造アクセスは、対応する非決定論的値で置換される。前記ループのループタイプに基づいてデータ構造の要素に作用する前記ループのループ制御ステートメントをなくすこと。

前記ループのループタイプが完全ループであると判断される実施形態例では、ループ制御ステートメントは、if（真）ステートメントで置換されて、ループ制御ステートメントをなくす。前記ループのループタイプが部分ループであると判断される別の実施形態例では、ループ制御ステートメントは、if（非決定論的）ステートメントで置換されて、ループ制御ステートメントをなくす。

複数の非アレイ割り当てをループ本体の冒頭及びソースコードのループ本体の後に追加すること。非アレイ割り当てをループ本体の冒頭及びソースコードのループ本体の後に追加する例は、図１を参照して説明される。２１２において、方法２００は、モデルチェックのために抽象化コードを提供することを含む。

データ構造抽象化の開示される方法及びシステムは、データ構造を含むアサーションを有するプログラムを検証することを可能にする。本明細書に開示される方法及びシステムは、アレイ要素に作用するループをなくすことにより、データ構造抽象化を提供する。抽象化は、プログラムの構文変形を介して実施される。データ構造抽象化プロセスでは、データ構造アクセス置換は、各データ構造アクセスを代表的な要素又は非決定論的値で置換する。データ構造アクセスを有するループは、適切なif条件で置換される。ループ内で変更された全ての他の変数には、非決定論的値が割り当てられる。アサーション「ａ」が、代表的な要素に対して違反しない場合、データ構造抽象化プロセスは非決定論的又は抽象化値を代表的な要素を含む全ての変数に割り当てるため、データ構造全体に対して当てはまる。したがって、データ構造抽象化プロセスを適用した後に生成されるプログラムコードは、元のプログラムの過剰近似であるように思われる。変換プログラムは、検証のために有界モデルチェッカーに入力される。

示されるステップは、示される例示的な実施形態を説明するために記載され、進行中の技術開発が、特定の機能が実行される様式を変更することを理解されたい。これらの例は、本明細書において、限定ではなく例示のために提示される。更に、機能構築ブロックの境界は、本明細書では、説明の便宜上、任意に定義されている。指定された機能及びその関係が適宜実行される限り、代替の境界を定義することができる。代替（本明細書に記載されるものの均等物、拡張形態、変形形態、逸脱等を含む）が、本明細書に含まれる教示に基づいて当業者に明らかになる。そのような代替形態は、開示される実施形態の範囲及び趣旨内に入る。また、「含む」、「有する」、「含有する」、及び「包含する」という単語、並びに他の同様の形態は、意味において均等であることが意図され、これらの単語の任意の１つに続く１つ又は複数の項目が、そのような１つ又は複数の項目の排他的なリストであることを意味せず、又は列挙された１つ又は複数の項目のみに限定されることを意味しないという点でオープンエンドである。本明細書及び添付の特許請求の範囲で使用される場合、単数形「１つの（a）」、「１つの（an）」、及び「その（the）」は、文脈により明らかに別段のことが示される場合を除き、複数形を含むことにも留意しなければならない。

更に、本開示と一貫して、１つ又は複数のコンピュータ可読記憶媒体を実施形態の実施に利用し得る。コンピュータ可読記憶媒体は、プロセッサが読み取り可能な情報又はデータを記憶し得る任意のタイプの物理的メモリを指す。したがって、コンピュータ可読記憶媒体は、本明細書に記載される実施形態と一貫するステップ又は段階をプロセッサに実行させる命令を含め、１つ又は複数のプロセッサにより実行される命令を記憶し得る。「コンピュータ可読媒体」という用語は、有形の物品を含み、搬送波及び一時的な信号を除外し、すなわち、非一時的であるものとして理解すべきである。例としては、ランダムアクセスメモリ（ＲＡＭ）、読み取り専用メモリ（ＲＯＭ）、揮発性メモリ、不揮発性メモリ、ハードドライブ、ＣＤ ＲＯＭ、ＤＶＤ、フラッシュドライブ、ディスク、及び任意の他の既知の物理的記憶媒体が挙げられる。

本開示及び例が、単なる例示としてみなされ、開示される実施形態の真の範囲及び趣旨が以下の特許請求の範囲により示されることが意図される。

１００ データ構造抽象化システム
１０２ プロセッサ
１０４ ＩＯインタフェース
１０６ メモリ
１０８ モジュール
１１０ データ

Claims (15)

1. ソースコードのモデルチェックのための前記ソースコードでのデータ構造抽象化のプロセッサにより実施される方法であって、
   １つ又は複数のハードウェアプロセッサによって、抽象化するソースコードを受信することと、
   前記１つ又は複数のハードウェアプロセッサによって、前記ソースコード内の１つ又は複数のデータ構造アクセスを識別することであって、前記１つ又は複数のデータ構造アクセスは、前記ソースコード内のデータ構造にアクセスするために、前記データ構造の要素を参照する表現を含み、前記１つ又は複数のデータ構造アクセスのうちのデータ構造アクセスは、アレイ、ハッシュテーブル、グラフ、ツリー、クラス、セット、及びマップのうちの１つを含む、識別することと、
   前記１つ又は複数のハードウェアプロセッサを介して、前記１つ又は複数のデータ構造アクセスを含む１つ又は複数のループを識別することであって、前記１つ又は複数のループは、制御ステートメント及びループ本体を含み、前記ループは、前記ループ本体を前記制御ステートメントに基づいて繰り返し実行させる、識別することと、
   前記１つ又は複数のハードウェアプロセッサを介して、前記１つ又は複数のループのループタイプを識別することであって、前記ループタイプは完全ループ及び部分ループを含み、前記完全ループは、前記データ構造の前記要素の全てにわたり繰り返されるループを含み、及び前記部分ループは、前記データ構造の前記要素のサブセットにわたり繰り返されるループを含む、識別することと、
   前記１つ又は複数のハードウェアプロセッサを介して、少なくとも前記ループタイプに基づいて抽象化コードを生成することであって、前記抽象化コードは、前記データ構造を抽象化することが可能であり、前記データ構造を抽象化することは、前記１つ又は複数のループの各ループについて、
   前記ループの反復でアクセスされる前記データ構造の要素に基づいて、前記１つ又は複数のデータ構造アクセスを前記ループの前記ループ本体内の非決定論的値又は、前記データ構造の代表的な要素で置換すること、
   前記ループのループタイプに基づいて、前記データ構造の前記要素に作用する前記ループのループ制御ステートメントをなくすこと、及び
   前記ループ本体の冒頭及び前記ソースコードの前記ループ本体の後に、複数の非アレイ代入を追加すること
   を実行することを含む、生成することと、
   前記１つ又は複数のハードウェアプロセッサを介して、モデルチェックのために前記抽象化コードを提供することと
   を含む、プロセッサ実施方法。
2. 前記ループの前記ループ制御ステートメントをなくすことは、
   前記ループの前記ループタイプが前記完全ループであると判断することと、
   前記ループ制御ステートメントをif（真）ステートメントで置換することと
   を含む、請求項１に記載の方法。
3. 前記ループの前記ループ制御ステートメントをなくすことは、
   前記ループの前記ループタイプが前記部分ループであると判断することと、
   前記ループ制御ステートメントをif（非決定論的）ステートメントで置換することと
   を含む、請求項１に記載の方法。
4. 前記データ構造アクセスの発生ロケーションを特定することを更に含み、前記ロケーションは、前記ソースコードのステートメントの左辺（ＬＨＳ）及び右辺（ＲＨＳ）のうちの一方である、請求項１に記載の方法。
5. 前記データ構造アクセスの前記発生ロケーションが前記ソースコードの前記ステートメントの前記右辺（ＲＨＳ）であると判断された場合に、
   前記アクセスされる要素が、前記ループの反復と異なる反復に関連付けられている場合、前記１つ又は複数のデータ構造アクセスを非決定論的値で置換することと
   を更に含む、請求項４に記載の方法。
6. 前記データ構造アクセスの前記発生ロケーションが前記ソースコードの前記ステートメントの前記左辺であると判断される場合に、前記１つ又は複数のデータ構造アクセスを前記データ構造の代表的な要素で置換することを更に含む、請求項４に記載の方法。
7. 前記ループ本体の前記冒頭及び前記ソースコードの前記ループ本体の後に、複数の非アレイ代入を追加する前に、
   前記ステートメントの前記左辺での前記ループ本体内の非データ構造変数を識別することと、
   非決定論的値を前記非データ構造変数に代入することと
   を更に含む、請求項４に記載の方法。
8. ソースコードのモデルチェックのための前記ソースコードでのデータ構造抽象化のシステムであって、
   １つ又は複数のメモリと、
   １つ又は複数のハードウェアプロセッサであって、前記１つ又は複数のメモリは前記１つ又は複数のハードウェアプロセッサに接続される、１つ又は複数のハードウェアプロセッサと
   を含み、前記１つ又は複数のハードウェアプロセッサは、前記１つ又は複数のメモリに記憶されたプログラム命令を実行して、
   抽象化するソースコードを受信することと、
   前記ソースコード内の１つ又は複数のデータ構造アクセスを識別することであって、前記１つ又は複数のデータ構造アクセスは、前記ソースコード内のデータ構造にアクセスするために、データ構造の要素を参照する表現を含み、前記１つ又は複数のデータ構造アクセスのうちのデータ構造アクセスは、アレイ、ハッシュテーブル、グラフ、ツリー、クラス、セット、及びマップのうちの１つを含む、識別することと、
   前記１つ又は複数のデータ構造アクセスを含む１つ又は複数のループを識別することであって、前記１つ又は複数のループは、制御ステートメント及びループ本体を含み、前記ループは、前記ループ本体を前記制御ステートメントに基づいて繰り返し実行させる、識別することと、
   前記１つ又は複数のループのループタイプを識別することであって、前記ループタイプは完全ループ及び部分ループを含み、完全ループは、前記データ構造の要素の全てにわたり繰り返されるループを含み、及び部分ループは、前記データ構造の要素のサブセットにわたり繰り返されるループを含む、識別することと、
   少なくとも前記ループタイプに基づいて抽象化コードを生成することであって、前記抽象化コードは、前記データ構造を抽象化することが可能であり、前記データ構造を抽象化することは、前記１つ又は複数のループの各ループについて、
   前記ループの反復でアクセスされる前記データ構造の要素に基づいて、前記１つ又は複数のデータ構造アクセスを前記ループの前記ループ本体内の非決定論的値又は、前記データ構造の代表的な要素で置換すること、
   前記ループのループタイプに基づいて、前記データ構造の前記要素に作用する前記ループのループ制御ステートメントをなくすこと、及び
   前記ループ本体の冒頭及び前記ソースコードの前記ループ本体の後に、複数の非アレイ代入を追加すること
   を実行することを含む、生成することと、
   モデルチェックのために前記抽象化コードを提供することと
   を実行することが可能である、システム。
9. 前記ループの前記ループ制御ステートメントをなくすために、前記１つ又は複数のハードウェアプロセッサは、
   前記ループの前記ループタイプが前記完全ループであると判断するプログラム命令と、
   前記ループ制御ステートメントをif（真）ステートメントで置換するプログラム命令と
   を実行することが可能である、請求項８に記載のシステム。
10. 前記ループの前記ループ制御ステートメントをなくすために、前記１つ又は複数のハードウェアプロセッサは、
    前記ループの前記ループタイプが前記部分ループであると判断するプログラム命令と、
    前記ループ制御ステートメントをif（非決定論的）ステートメントで置換するプログラム命令と
    を実行することが可能である、請求項８に記載のシステム。
11. 前記１つ又は複数のハードウェアプロセッサは、前記データ構造アクセスの発生ロケーションを特定するプログラム命令を実行することが可能であり、前記ロケーションは、前記ソースコードのステートメントの左辺（ＬＨＳ）及び右辺（ＲＨＳ）のうちの一方である、請求項８に記載のシステム。
12. 前記データ構造アクセスの前記発生ロケーションが、前記ソースコードの前記ステートメントの前記右辺（ＲＨＳ）であると判断された場合に、前記１つ又は複数のハードウェアプロセッサは、
    前記アクセスされる要素が、前記ループの反復と異なる反復に関連付けられている場合、前記１つ又は複数のデータ構造アクセスを非決定論的値で置換するプログラム命令と
    を実行することが可能である、請求項１１に記載のシステム。
13. 前記データ構造アクセスの前記発生ロケーションが、前記ソースコードの前記ステートメントの前記左辺であると判断される場合に、前記１つ又は複数のハードウェアプロセッサは、前記１つ又は複数のデータ構造アクセスを前記データ構造の代表的な要素で置換するプログラム命令を実行することが可能である、請求項１１に記載のシステム。
14. 前記ループ本体の前記冒頭及び前記ソースコードの前記ループ本体の後に、複数の非アレイ代入を追加する前に、前記１つ又は複数のハードウェアプロセッサは、
    前記ステートメントの前記左辺での前記ループ本体内の非データ構造変数を識別するプログラム命令と、
    非決定論的値を前記非データ構造変数に代入するプログラム命令と
    を実行することが可能である、請求項１１に記載のシステム。
15. 非一時的コンピュータ可読媒体であって、ソースコード内のデータ構造抽象化の方法を実行するコンピュータプログラムを具現した非一時的コンピュータ可読媒体であって、前記方法は、
    抽象化するソースコードを受信することと、
    前記ソースコード内の１つ又は複数のデータ構造アクセスを識別することであって、前記１つ又は複数のデータ構造アクセスは、前記ソースコード内のデータ構造にアクセスするために、前記データ構造の要素を参照する表現を含み、前記１つ又は複数のデータ構造アクセスのうちのデータ構造アクセスは、アレイ、ハッシュテーブル、グラフ、ツリー、クラス、セット、及びマップのうちの１つを含む、識別することと、
    前記１つ又は複数のデータ構造アクセスを含む１つ又は複数のループを識別することであって、前記１つ又は複数のループは、制御ステートメント及びループ本体を含み、前記ループは、前記ループ本体を前記制御ステートメントに基づいて繰り返し実行させる、識別することと、
    前記１つ又は複数のループのループタイプを識別することと、
    少なくとも前記ループタイプに基づいて抽象化コードを生成することであって、前記抽象化コードは、前記データ構造を抽象化することが可能であり、前記データ構造を抽象化することは、前記１つ又は複数のループの各ループについて、
    前記ループの反復でアクセスされる前記データ構造の要素に基づいて、前記ループの前記ループ本体内の非決定論的値又は、前記データ構造の代表的な要素で前記１つ又は複数のデータ構造アクセスを置換すること、
    前記ループのループタイプに基づいて、前記データ構造の前記要素に作用する前記ループのループ制御ステートメントをなくすこと、及び
    前記ループ本体の冒頭及び前記ソースコードの前記ループ本体の後に、複数の非アレイ代入を追加すること
    を実行することを含む、生成することと、
    モデルチェックのために前記抽象化コードを提供することと
    を含む、非一時的コンピュータ可読媒体。

Images