(57)【特許請求の範囲】
【請求項１】
安全重視ソフトウェアのモデルベース設計のための方法であって、
自然言語ソフトウェア要件（１３２）を受信することと、
前記自然言語ソフトウェア要件（１３２）の意味モデリング（１５０）およびグラフィックモデリング（１５２）の少なくとも１つを実装することによって構造化自然言語でソフトウェア仕様モデル（１３３）を開発することと、
前記ソフトウェア仕様モデル（１３３）の形式要件解析を適用することと、
前記ソフトウェア仕様モデル（１３３）から要件ベースのテストケース（１４６）を自動的に生成することと、
前記ソフトウェア仕様モデル（１３３）に基づいてソフトウェア設計モデル（１３４）を開発することと、
前記ソフトウェア設計モデル（１３４）の形式解析を実施することと、
前記ソフトウェア設計モデル（１３４）に自動的に生成した要件ベースのテストケース（１４６）を適用して、前記ソフトウェア設計モデル（１３４）の機能及び、カバレッジを解析することと、
前記ソフトウェア設計モデル（１３４）を使用してソースコード（１３６）を自動生成することと、
前記自動生成されたソースコード（１３６）から実行可能オブジェクトコード（１３８）をコンパイルすることと、
を含み、
前記ソフトウェア設計モデル（１３４）の機能及び、カバレッジの解析が、
前記ソフトウェア設計モデル（１３４）及び前記自動的に生成した要件ベースのテストケース（１４６）の欠陥または不整合を特定する誤りを自動的に特定することと、
前記ソフトウェア設計モデル（１３４）及び前記自動的に生成した要件ベースのテストケース（１４６）の誤りを修正することと、
前記カバレッジを満足させる追加のテストケースを自動的に生成することを含む、方法。
【請求項２】
前記ソフトウェア仕様モデル（１３３）から前記テストケース（１４６）を自動生成する自動化テストケースおよび手順生成ユニット（１５６）を含む、請求項１記載の方法。
【請求項３】
自然言語ソフトウェア要件（１３２）の意味モデリング（１５０）および、自然言語ソフトウェア要件（１３２）のグラフィックモデリング（１５２）の両方を実装することによって構造化自然言語で前記ソフトウェア仕様モデル（１３３）が開発され、
自動化定理証明技術を実装して前記ソフトウェア仕様モデル（１３３）の整合性、正当性および完全性の少なくとも１つを解析および検証する自動化定理証明ユニット（１５４）を含む、請求項１または２に記載の方法。
【請求項４】
前記ソフトウェア仕様モデル（１３３）の解析の結果が満足でなければ、次いで前記ソフトウェア仕様モデル（１３３）を調節して前記自然言語ソフトウェア要件（１３２）に関する任意の不整合を修正することを含み、
前記調節したソフトウェア仕様モデル（１３３）に前記形式要件解析を適用することを含む、
請求項１乃至３のいずれかに記載の方法。
【請求項５】
前記ソフトウェア設計モデル（１３４）に適用される前記テストケースを自動生成する自動化要件ベースのテストケースおよび手順生成ユニット（１５６）を含む、請求項１乃至４のいずれかに記載の方法。
【請求項６】
モデル検査技術を使用して前記ソフトウェア設計モデル（１３４）に適用される前記要件ベースのテストケース（１４６）を生成することを含む、請求項１乃至５のいずれかに記載の方法。
【請求項７】
前記ソフトウェア設計モデル（１３４）の解析の結果が満足でなければ、次いで前記ソフトウェア設計モデル（１３４）を調節して前記ソフトウェア仕様モデル（１３３）に関する任意の不整合を修正することを含み、
前記調節したソフトウェア設計モデル（１３４）に前記テストケースを適用することを含む、請求項１乃至６のいずれかに記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は安全重視ソフトウェアシステム開発に関する。
【背景技術】
【０００２】
マイクロプロセッサ制御機器の広汎性によりますますより有能な装置に至ったが、しかしそれはまた、これらの組込みシステムを制御するソフトウェアの品質により強く依存する。多くの潜在的に危険な一部機器は組込みソフトウェアによって制御される（たとえば、車、列車、飛行機、製油所、化学処理工場、原子力発電所および医療装置など）。これらの装置およびシステムのための運用アプリケーションコードの正当性を検証するための従来の手法は困難かつ非効率である。
【０００３】
安全重視ソフトウェアシステム開発はこれらのシステムの大きさおよび複雑さの増大に対処し、かつ安全重視運用を維持する必要を考慮に入れる。複雑で重要なシステムを開発するために、一定の範囲のソフトウェア工学方法、ツールおよび体系がある。たとえば、１つの方法は安全重視システム開発にモデル駆動工学技術を適用している。
【０００４】
従来の手法は市販の総合設計環境（ＩＤＥ）ツールを使用してソフトウェア仕様モデリング、確認／検証、ならびにテストケース生成および実行を行うことを含むことができる。典型的に、これらのツールは厳密な方法を使用して詳細設計ステップの一部分を自動化または半自動化する一方で、データ入力要件を軽減して残りのステップの時間を節約する。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】米国特許第８９４３４６５号公報
【発明の概要】
【課題を解決するための手段】
【０００６】
実施形態に従って、システムおよび方法は安全重視ソフトウェアの開発およびテスト生成のためのモデルベース自動化設計過程を提供する。実施形態としてのシステムおよび方法は領域特定オントロジおよび形式検証方法を利用して最上位要件を改善および拡張する。これらのシステムおよび方法は、ソフトウェアを書く前に要件ベーステストを自動的に生成する基礎として、検証可能な仕様モデル（それゆえに「モデルベース」という名称）を活用する。実施形態に従って、要件ベーステストが仕様モデルから生成される。ソフトウェアを開発するために設計モデルを使用する。これらのステップの厳密さおよび自動化は改善したソフトウェア設計および低減したテスト労力という結果になり、安全重視ソフトウェア開発者にとっての時間および費用を節約する。
【０００７】
実施形態としての過程に形式的方法および論理モデルを組み込むことによって、仕様要件の誤りを識別することができ、そして要件を整合性および完全性に関して検証することができる。誤りを識別した上で、要件を、それらが再テストされるときに論理的に完全でありかつ整合するまで、必要ならば反復して訂正することができる。オントロジ、意味ネットおよびカバレッジ解析はすべて、不完全である要件を拡張するための明示的な情報を提供する。
【０００８】
実施形態としてのシステムおよび方法は「安全ケース」を要件および対応する検証ステップ（たとえば、モデルベース設計）に組み込むことができる。複雑な時間的関係（たとえば、同時性要件および／または能力）を表現することもできる。
【０００９】
一旦ソフトウェア仕様要件が完全でありかつ整合すると、設計モデルおよびその後の検証／確認テストをソースコードの検査のために生成することができる。ソースコードは指定された設計のより詳細な表現として見ることができ、同設計要件を実施するオブジェクトおよび／または実行可能コードという結果になる。
【００１０】
実施形態としての手法は検証／確認活動の間に検出される誤りの減少という結果になる。実施形態としてのシステムおよび方法はこれらの過程を自動化し、従来の手動ツール支援コード生成と比較して設計要件を満たす際のより高精度ならびに修正およびテストする際のより高速度を提供することによって開発関連の労働および時間費用の減少を提供するより厳密な設計／検証／確認過程という結果になる。
【００１１】
実施形態としてのモデルベースシステムおよび方法は自然言語ベース文の代わりに、運用、設計およびテスト生成要件を定義する数学的に厳密な形式的論理文を用い、したがって早期の設計過程の間に、要件の品質、厳密さ、整合性および範囲を改善する機会を提供する。
【図面の簡単な説明】
【００１２】
【図１】実施形態に従う安全重視ソフトウェアのモデルベース設計のためのシステムを描く。
【図２】実施形態に従う安全重視ソフトウェアのモデルベース設計のための過程のフローチャートを描く。
【図３】実施形態に従うモデルベース開発過程のためのフローチャートを描く。
【発明を実施するための形態】
【００１３】
図１は、実施形態に従う安全重視コンピュータソフトウェア開発のためのシステム１００を描く。システム１００は、コンピュータ（ローカルに動作する単一のコンピュータ１１０か、または電子通信ネットワーク１２０（たとえば、インターネット）によって共に連結されるいくつかのコンピュータ１１２、１１４、１１Ｎ）、安全重視ソフトウェアの明細−たとえばソフトウェアに割り当てられるシステム要件（ＳＲＡＴＳ）１３２、ソフトウェア仕様モデル１３３、設計モデル１３４、自動生成されるソースコード１３６、実行可能オブジェクトコード１３８−を含むことができる関連データベース１３０を含むことができる。システム１００は、意味ネット１４２、オントロジ１４４、要件ベーステストケース１４６および自動生成されるモデルカバレッジテストケース１４８を含むことができるデータベース１４０も含むことができる。データベース１３０およびデータベース１４０は２つのデータベースとして描かれるけれども、いくつかの実装では１つのデータベースがすべての記憶を含むことができ、他の実装では３つ以上のデータベースをシステム１００に含めることができる。
【００１４】
実装に従って、単一のコンピュータ１１０は、モデルベース安全重視ソフトウェア設計を実装する動作を行うように構成される構造ユニットを含むことができる。これらのユニットは、意味モデリングユニット１５０、グラフィックモデリングユニット１５２、自動化定理証明（ＡＴＰ）ユニット１５４、自動化テストケースおよび手順生成（ＡＴＣＰＧ）ユニット１５６、ならびに自動化コード生成ユニット１５８を含むことができる。他の実装では、これらのユニットは、電子通信ネットワークによって共に連結されるいくつかのコンピュータの間で分散することができる。
【００１５】
図２は、実施形態に従う安全重視ソフトウェアのモデルベース設計のための過程２００のフローチャートを描く。過程２００は自然言語ＳＲＡＴＳを解析し、検証および容認後に設計モデルの基礎となる仕様モデルを開発する。用語「設計モデル」（本明細書で使用する場合）は、オブジェクトモデルまたは統一モデリング言語（ＵＭＬ）モデルなどの概念モデルである。設計モデルは、アプリケーションソフトウェアによって行われるべきエンティティおよび機能変換を描くことができる。
【００１６】
設計モデルから、まずソースコードを過程２００によって自動生成することができ、そして次いで実行可能オブジェクトコード（ＥＯＣ）を同様に生成することができる。過程２００は設計、ソースコードおよびＥＯＣを検証することができる。この要件ベース過程から生じるＥＯＣはその後ＥＯＣベース検査方法を受けることができ、それは追加のフィードバックを提供することができる。
【００１７】
仕様モデルをステップ２０５で取り込む。取込みには、システムに提供されるテキスト形式の自然言語システム要件ＳＲＡＴＳの確認を含むことができる。意味モデリングユニット１５０および／またはグラフィックモデリングユニット１５２は意味およびグラフィックモデリング技術を実装してＳＲＡＴＳから仕様モデルを開発する。仕様モデルは、意味モデルを含みかつグラフ形状で見るまたは編集することができる構造化自然言語で実装する。
【００１８】
仕様モデルに対する形式要件解析をステップ２１０で行う。仕様モデルは、自動化定理証明技術を実装するＡＴＰユニット１５４によって正当性および整合性に関して解析および検証することができる。仕様モデルからのテストケースを、ステップ２１５で、ＡＴＣＰＧユニット１５６によって自動生成する。実施形態に従って、システムはＡＴＣＰＧを利用して設計モデル自体の要件のためのテストケースを自動生成することができる。他の実装では、自動生成したテストケースは、モデル検査または他の形式解析技術を使用してシステム１００によって自動的に生成することができる。万一要件解析および／または生成したテストケースにより、モデルが必要とされるほど堅牢でないこと（すなわち、ソフトウェア仕様モデルが必要な整合性、正当性および／または完全性を欠いていること）が示されれば、過程２００はステップ２０５に戻って仕様モデルをさらに取り込むことができる。
【００１９】
要件解析により要件が完全でありかつ自己整合していることが示された後、仕様モデルはステップ２２０でソフトウェア設計モデルの開発の基礎となる。テストケースを仕様モデルから生成し、そして設計モデルに適用する。テストケースを設計モデルに適用した後、ステップ２２５で、モデルカバレッジをその性能に基づいて解析する。任意の欠陥または不整合を修正することができ、次いでテストケースシナリオを繰り返すことによって、ステップ２３０で、設計モデルを検証することができる。
【００２０】
検証した設計モデルを自動化コード生成ユニット１５８によって使用して、ステップ２３５で、安全重視ソフトウェアのためのソースコードを自動生成する。システム１００は次いで、ステップ２４０で、静的解析技術を使用してソースコードを検証する。ステップ２４５で、検証したソースコードから実行可能オブジェクトコードをコンパイルする。
【００２１】
図３は、実施形態に従うモデルベース開発過程３００のためのフローチャートを描く。安全重視コンピュータソフトウェア開発のためのシステム１００は、モデルベース開発過程３００の段階３０５、３１０、３２５、３３０、３４５、３５５、３６５から設計情報を受信するコンピュータ実装アプリケーション３１５、３２０、３３５、３４０、３５０、３６０、３７０を含むことができる。いくつかの実装では、受信した設計情報は、システム１００の人間ユーザからの追加の指令および／または命令で補足することができる。受信した設計情報に基づいて、システム１００のコンピュータ実装アプリケーションによって処理されるように、過程３００は新しい結果を生成することができる−たとえば完全性の確定、設計モデル、新しいソフトウェアテスト、および／または設計過程の特定の段階の設計データの欠点または不完全性を特定する欠陥を識別するメッセージ。
【００２２】
欠陥識別メッセージが生成されれば、過程３００は次いで直前のステップ（過程３００内の様々な過程ステップを接続する両矢印によって示される）のデータに戻る。欠陥は、コンピュータ実装過程３００によって提供される勧告に従って人間ユーザによって修正することができる。
【００２３】
ステップ３０５で過程３００に提供される初期ＳＲＡＴＳデータは自然言語文書を含む。安全重視コンピュータソフトウェア開発のためのシステム１００はソフトウェアを自動的に生成し、かつ早期の段階で生成した他の診断情報または資料と同様にテストケースを自動的に生成する。このソフトウェア、テストケース、他の診断情報および資料は提供されたＳＲＡＴＳに基づいている。システム１００によって実装されるような過程３００は設計過程の手動作用の減少で安全重視ソフトウェア設計を改善する。自動化開発を達成するために、実施形態に従って、過程３００はコンピュータ実装アプリケーションすなわち、顧客モデルベース確認（ステップ３１５）、形式要件解析（ステップ３２０）、形式設計検証（ステップ３３５）、モデルカバレッジ解析（ステップ３４０）、テストベース設計モデル検証（ステップ３５０）、形式コード検証（ステップ３６０）、テストベースＥＯＣ検証（ステップ３７０）を含む。
【００２４】
過程３００は、ハードウェアおよびソフトウェア両方の能力を含むより高レベルのシステム要件から派生されるテキスト形式の自然言語文書ＳＲＡＴＳを、ステップ３０５で受信することで開始する。ＳＲＡＴＳから、ステップ３１０で、意味モデリングおよびグラフィックモデリング技術の組合せを使用して仕様モデルを開発する。実施形態に従って、過程３００を実装するシステム１００は、高レベル要件（ＨＬＲ）をテキストとして取り込むことの必要性を排除した。実施形態に従って、従来のＨＬＲは人間および機械可読仕様モデルに置き換えられる。
【００２５】
仕様モデルをステップ３１５で確認する。確認は、ユーザに提示する要件の解析表現（たとえば、オントロジおよび意味ネット）の助けを借りて行うことができる。仕様モデルを、ステップ３２０で、ＡＴＰアプリケーションを使用して正当性および整合性に関して形式的に解析および検証する。このステップは要件の誤りを過程の初期に識別し、かつ後期サイクル再処理を有意に低減させることができる。
【００２６】
要件解析３２０から仕様モデル取込み３１０へのフィードバックループがある。このフィードバックループはリアルタイムフィードバックを提供して誤りに対してエンジニアに警告する。
【００２７】
確認および形式要件解析後に、仕様モデルは入力として進み、ステップ３３０で設計モデルを作成する。設計モデルを、ステップ３３５で、モデル検査を使用して形式的に検証する。仕様モデルは、ステップ３２５で、要件ベース自動化テストケース生成過程への入力としても使用される。テストケースおよび手順を自動的に生成する（たとえば、モデル検査技術を使用して）。テストケースを次いで、ステップ３５０で、設計モデルに適用し、そして正しい機能性に関して解析する。
【００２８】
要件ベーステストケース生成機能３２５から仕様モデル３１０への別のフィードバックループがあり、仕様モデルを検証するために必要とされるテストケースの数に比例している検証複雑性メトリックを示す。要件取込みエンジニアはこの情報を使用して、検証費用／複雑性を低下させるために仕様モデルを単純化してもよい。実装に従って、要件取込みツールは、検証がより容易（より少ないテストケース）だろう原理で同じ情報を取り込む提案オプションを提供することもできる。
【００２９】
誤りを検出すると、設計モデルを修正する。一連のステップを行う、または同時ステップの順序を予測することができない場合に欠陥および不整合を検出することがあり、これらの場合シーケンスを後退することによって、またはそうでなければ無順序のステップの時間的順序付けを実施することによって設計モデル修正を行ってもよい。次に、テストケースを設計モデルに適用し、そしてモデルカバレッジに関して解析する（ステップ３４０）。このステップは、（ａ）要件ベーステストケース、仕様モデルおよび／または設計モデルの誤り（たとえば、意図しない機能性、不要コードなど）、または（ｂ）派生要件に基づいてカバレッジの隙間を識別することができる。派生要件の場合、テストケースをステップ３４５で自動的に生成してモデルカバレッジを満足させる。
【００３０】
自動化テスト生成ツールを使用して、エンジニアが到達不能コードを識別するのを援助する、かつモデルの特定の部分を実行するだろうテストベクトルを識別することができる。適格の自動コード生成ツールを使用して、ステップ３５５で設計モデルからソースコードを作成する。ソースコードを、ステップ３６０で、静的解析技術を使用して形式的に解析する。ソースコードを、ステップ３６５で、ＥＯＣにコンパイルする。過程の初期に開発したテストスイートを再適用することによって、ステップ３７０で、テストベースＥＯＣ検証を行う。一旦検証を行うと、コンパイルしたＥＯＣを次いで従前のユニット、サブシステムおよびシステム検査に委ねることができる。
【００３１】
実施形態に従うシステムおよび方法は、コードの生成前にソフトウェア要件の整合性、正当性および／または完全性を検証する問題に厳密な数学的かつ論理的モデリング技術を適用する。実装に従って、一まとまりのツールが予備設計、解析およびソフトウェア生成のすべての段階を包含することができる。事前検証により、自動コード生成の使用および設計過程でのフィードバックの使用が実用的になる。実施形態としての過程およびシステムは概念および予備設計過程の間に誤りを検出することができる。これらの検出した誤りの修正は、コードを生成する前に設計情報を拡張、改善、修正および／または完成することができる。
【００３２】
いくつかの実施形態に従って、不揮発性メモリまたはコンピュータ可読媒体（たとえば、レジスタメモリ、プロセッサキャッシュ、ランダムアクセスメモリ、リードオンリメモリ、コンパクトディスクリードオンリメモリ、ハードドライブ、フラッシュメモリ、磁気媒体など）に記憶されるコンピュータプログラムアプリケーションは、実行されると、上述の通り、コントローラまたはプロセッサに安全重視ソフトウェアのモデルベース設計のための方法などの本明細書に論じられる方法を行うように命令してもかつ／または至らせてもよいコードまたは実行可能命令を含んでもよい。
【００３３】
コンピュータ可読媒体は、すべての形態および種類のメモリならびに一時的な伝播信号を除くすべてのコンピュータ可読媒体を含む非一時的なコンピュータ可読媒体でもよい。一実装では、不揮発性メモリまたはコンピュータ可読媒体は外部メモリでもよい。
【００３４】
特定のハードウェアおよび方法を本明細書に説明してきたが、任意の数の他の構成が本発明の実施形態に従って提供されてもよいことに留意されたい。したがって、本発明の基本的な新規の特徴を図示、説明および指摘してきたが、例示した実施形態の形態および詳細の、ならびにそれらの動作の様々な省略、置換および変化が、本発明の趣旨および範囲から逸脱することなく当業者によってなされてもよいことが理解されるだろう。一実施形態から別のものへの要素の置換も完全に意図および企図される。本発明は本明細書に添付の請求項およびその詳述の均等物に関して定められるのみである。
【符号の説明】
【００３５】
１００  安全重視コンピュータソフトウェア開発システム
１１０  コンピュータ
１１２  コンピュータ
１１４  コンピュータ
１１Ｎ  コンピュータ
１２０  電子通信ネットワーク
１３０  データベース
１３２  ソフトウェアに割り当てられるシステム要件
１３３  ソフトウェア仕様モデル
１３４  設計モデル
１３６  自動生成されるソースコード
１３８  実行可能オブジェクトコード
１４０  データベース
１４２  意味ネット
１４４  オントロジ
１４６  要件ベーステストケース
１４８  自動生成されるモデルカバレッジテストケース
１５０  意味モデリングユニット
１５２  グラフィックモデリングユニット
１５４  自動化定理証明ユニット
１５６  自動化テストケースおよび手順生成ユニット
１５８  自動化コード生成ユニット
【図１】
0006621204.tif 000002
【図２】
0006621204.tif 000003
【図３】
0006621204.tif 000004