(57)【要約】【課題】例えば航空電子工学システムの制御のために使用するソフトウエアに基づくコードを開発する方法を提供する。【解決手段】検証されるソフトウエアコードの開発は非常に困難な処理であり、安全上重大なアプリケーションが関係する場合には特に重要である。要件に対して検証されたソフトウエアコードを生成する方法が提供され、本方法は、ｉ）前記要件の状態モデルを生成するためにソフトウエアを使用するステップと、ｉｉ）前記状態モデルのソフトウエアコード表現と、前記状態モデルの数学的表現とを開発するために前記状態モデルを使用するステップと、ｉｉｉ）前記ソフトウエアコード表現が、前記数学的表現の正確な実現であることを検証するために、前記ソフトウエアコード表現と前記数学的表現とを比較するステップとを含むことを特徴としている。【特許請求の範囲】
【請求項１】
要件に対して検証されたソフトウエアコードを生成する方法であって、
ｉ．前記要件の状態モデルを生成するためにソフトウエアを使用するステップと、
ｉｉ．前記状態モデルのソフトウエアコード表現と、前記状態モデルの数学的表現とを開発するために前記状態モデルを使用するステップと、
ｉｉｉ．前記ソフトウエアコード表現が、前記数学的表現の正確な実現であることを検証するために、前記ソフトウエアコード表現と前記数学的表現とを比較するステップとを含むことを特徴とする方法。
【請求項２】
デッドロック及びライブロックのような状態関連エラーがないことを実証するためにモデルチェッキングを実行する付加的ステップを含むことを特徴とする請求項１に記載の方法。
【請求項３】
前記要件の状態モデルを生成するのに使用されるソフトウエアは、Ｓｔａｔｅｆｌｏｗ（Ｒ）であることを特徴とする請求項１又は請求項２のいずれか１項に記載の方法。
【請求項４】
前記状態モデルのソフトウエアコード表現は、ＲａｖｅｎＳＰＡＲＫ  Ａｄａを使用して生成されることを特徴とする請求項１〜請求項３いずれか１項に記載の方法。
【請求項５】
前記状態モデルの数学的表現は、「Ｃｉｒｃｕｓ」又は他の同等な形式的言語を使用して生成されることを特徴とする請求項１〜請求項４いずれか１項に記載の方法。
【請求項６】
前記生成された検証ソフトウエアコードは、ソフトウエア制御コードであることを特徴とする請求項１〜請求項５いずれか１項に記載の方法。
【請求項７】
検証されたソフトウエアコードを生成する方法であって、
ｉ．要件のステートメントを開発するステップと、
ｉｉ．前記要件のステートメントから状態モデルを生成するためにソフトウエアを使用するステップと、
ｉｉｉ．前記状態モデルから数学的表現で形式的仕様を開発するステップと、
ｉｖ．前記状態モデルを表現するソフトウエアコードを開発するために、前記状態モデルを使用するステップと、
ｖ．検証条件を準備するために、前記数学的表現と前記開発されたソフトウエアコードとを使用して適合引数を構成するステップと、
ｖｉ．前記数学的表現と前記開発されたソフトウエアコードとの間に不一致がある場合に、新たなソフトウエアコードを生成するステップと、
ｖｉｉ．前記新たなソフトウエアコードが、前記数学的表現と前記要件のステートメントとの正確な表現であることを証明するために、前記検証条件を履行するステップとを含むことを特徴とする方法。
【請求項８】
前記形式的仕様においてモデルチェッキングを実行する付加的なステップを含むことを特徴とする請求項７に記載の方法。
【請求項９】
請求項１〜請求項８のいずれか１項に従って生成されたことを特徴とする検証されたソフトウエアコード。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、例えば航空電子工学システムの制御のために使用するソフトウエアコードを開発する方法及びその実現に関する。
【背景技術】
【０００２】
ハードウエアの制御機能に関するソフトウエア実現は、より複雑な制御オペレーションを提供するためのソフトウエア依存度が高くなるにつれて年々ますます複雑になってきている。その結果、複雑な制御オペレーションに対応するための多量のソフトウエアコードが開発されてきた。
【０００３】
そのような例の１つは、「ユーロファイター」などの近代戦闘機における航空電子工学システムでの実現用のソフトウエアコードの開発である。このような航空機の性能特性は、空気力学的に不安定な状態でのシステムオペレーションによって可能になる。これには、非常に複雑で大量のコンピュータソフトウエアの支援が必要となる。このようなソフトウエアの開発と検証は、非常に時間のかかる処理になる可能性がある。「ユーロファイター」の場合、フライト制御システムは、１２年以上も開発されてきている。
【０００４】
安全上重大なシステムを含め、エラーやバグのないソフトウエアは絶対にないことは周知の事実である。これは、過去に起きたリアルタイム又は非リアルタイムシステムにおける陸上、海上、又は空中の多くのスリルあふれる失敗によって証明される。結果として、ソフトウエアが全ての環境で期待通りに作動することを判断するために、大規模な検証処理が必要である。そのような検証は、ソフトウエアが最初に開発された時、及び、ソフトウエア又はそれが作動するシステムの変更の度に必要になる。これは、ソフトウエアのオペレーション方法が正しいと検証されることを保証する手助けとなるだろう。
【０００５】
ソフトウエアに関する要件は、システムの仕様から得られる。ソフトウエア要件が最終的になると、前記ソフトウエア要件についての数学的表現の仕様が記載される。次に、仕様を正確に反映するためのソフトウエアコードが開発される。特に安全上重大なソフトウエアにとって、これは、普通は手作業でなされる困難な処理である。これは、どのソフトウエアの開発においても非能率的な方法である。
【０００６】
およそ２０年前、フォーマルメソッド（ＦＭ）として公知のソフトウエア開発に対する数学的アプローチが、ソフトウエアのコードが仕様を正確に反映するという確証を得るための可能性のある方法として出現していた。ＦＭは、数学的な表現で書かれた形式的な仕様を用いている。その形式的仕様から、種々の数学的手法を使用して、形式的仕様を正確に反映するソフトウエアコードを生成することが可能である。この数学的手法には、証明が為されることになり、検証と呼ばれる技術である。
【０００７】
しかしながら、ＦＭが理解されるのがとても難しい理由から、ＦＭは、広範囲に使用できるフォーマットには開発されておらず、ほとんど学問的な領域に留まっている。ＦＭは、概念的に難しい数学の部門を用いていて、これがおそらくその使用を億劫にし、より広範囲に容認されないのであろう。特に、証明を与えることは骨が折れて時間がかかり、極端に熟練を要する処理である。更に、ＦＭは、小さなアプリケーションの場合でも扱いにくい可能性があり、熟練者の不足から実行するのに高価なものになっている。
【０００８】
前述した結果は、製造者にしてみれば、ソフトウエア方法によって安全上重大な処理を実行することは明らかに気が進まないことであった。しかしながら、最近２、３年で、自動ソフトウエア開発の分野が進歩した。特に、英国ウスターシア、モルバーン所在の国防評価研究機関（ＤＥＲＡ）は、正式検証フライト制御法則コードの自動導出ツールを開発してきた。このアプローチは、「ユーロファイター」用のフライト制御システムを検証するために使用されている。
【０００９】
それは、現存する市販ソフトウエアパッケージを使用して、Ｓｉｍｕｌｉｎｋ（Ｒ）モデルを生成することによって作動する。Ｓｉｍｕｌｉｎｋ（Ｒ）は、ザ・マスワークス・インコーポレーテッドの製品であるＭＡＴＬＡＢ（Ｒ）として公知の市販ソフトウエアパッケージの一部を形成する。
Ｓｉｍｕｌｉｎｋ（Ｒ）モデルは、ソフトウエア要件の数学的表現である。Ｓｉｍｕｌｉｎｋ（Ｒ）は、コンピュータプログラム言語であるＳＰＡＲＫ  Ａｄａコードを自動的に生成する。
【００１０】
Ｓｉｍｕｌｉｎｋ（Ｒ）モデルはまた、「Ｚ」と呼ばれる数学的言語で形式的な仕様を自動的に生成するために、ＣｌａｗＺと呼ばれるツールによって使用される。ＣｌａｗＺは、Ｓｉｍｕｌｉｎｋ（Ｒ）モデル及び「Ｚ」間の制御法則モデルの表現を翻訳するＤＥＲＡによって開発されたツールである。「Ｚ」とＳＰＡＲＫ  Ａｄａの形式的仕様は互いに比較され、ＳＰＡＲＫ  Ａｄａは、ＰｒｏｏｆＰｏｗｅｒ（Ｒ）内の適合表記ツールを用いた適合引数を構成することを要求されるよう変更されるが、これは自動的に行われる。ＰｒｏｏｆＰｏｗｅｒ（Ｒ）は、レンマ１リミテッドの製品である。
【００１１】
適合表記ツールは、次に、適合可能なファイル及び検証条件（ＶＣ）として、前記変更済みのＳＰＡＲＫ  Ａｄａを生成する。ＰｒｏｏｆＰｏｗｅｒ（Ｒ）の定理証明部分を使用することによって、ＶＣが数学的に「真」であるという数学的な証明を支援するソフトウエアツールを実行することが可能である。従って、これは、変更済みＳＰＡＲＫ  Ａｄａコードが、形式的仕様の正しい表現、すなわちＳｉｍｕｌｉｎｋ（Ｒ）モデルであることを確認するか、或いは確認しない。前記証明における労力の多くは、自動化されている。
【００１２】
前述のものとは別に、ソフトウエア要件から開発される状態に基づくモデリングの使用によって、市販ソフトウエアパッケージの開発に関する作業が行われてきている。
【００１３】
状態モデルの概念は、例示の方法によって最も良く説明されている。つまり、本明細書での例は、航空機用ジェットエンジンの逆スラスト装置に関するものである。逆スラスト装置の状態モデルは、前記逆スラスト装置が占有できる各‘状態’（例えば、状態１：解放状態、状態２：部分的拘束状態、状態３：完全拘束状態）を設計し、そして、それは、各状態内及び各状態間の移行において許容できる動作を支配する「規則」の対応リストを伴っている。この同じ原理が、ソフトウエアコードの開発とオペレーションに対しても適用できる。
【発明の開示】
【課題を解決するための手段】
【００１４】
従って、要件に対して検証されるソフトウエアコードを生成する方法が提供され、本方法は、
ｉ．前記要件の状態モデルを生成するためにソフトウエアを使用するステップと、
ｉｉ．前記状態モデルのソフトウエアコード表現と、前記状態モデルの数学的表現とを開発するために前記状態モデルを使用するステップと、
ｉｉｉ．前記ソフトウエアコード表現が、前記数学的表現の正確な実現であることを検証するために、前記ソフトウエアコード表現と前記数学的表現とを比較するステップとを含んでいる。
【００１５】
相互作用して複数が同時に動作する構成要素を有するシステムを開発する時に、ライブロック及びデッドロックなどのエラーが発生する可能性がある。このようなエラーにより、性能が劣化して挙動が予測不能となり、システムの故障につながる。そのような問題を回避するために、モデルチェッキングとして知られた手法を利用することができるが、このモデルチェッキングは、有限状態の同時システムを形式的に検証するための手法である。従って、前述の方法は、デッドロック及びライブロックなどの状態関連エラーがないことを実証するために、モデルチェッキングを実行する付加的なステップを含んでいる。
【００１６】
前記方法は、状態に基づくモデリングの使用により、ソフトウエアコードの自動開発を可能にする。これは、安全上重大なソフトウエアの分野で特に有効であるが、任意のソフトウエアの開発に利用できない理由はない。それは、（「ＦＭ」のような）現存の方法を使用するのに比べて開発時間を大幅に短縮させることにより、ソフトウエア開発コストの大幅な低減をもたらすことになる。それはまた、任意の変更が要件レベルで行われ、残された作業の大部分は自動化されるとき、装置の通し寿命に亘るコストを低減するのに特に有効である。特に、本方法は、航空電子工学システムの分野で有用である。従って、本方法は、生成された検証ソフトウエアコードがソフトウエア制御コードであるように使用することができる。
【００１７】
前記状態モデルは、Ｓｔａｔｅｆｌｏｗ（Ｒ）などの適切な市販ソフトウエアパッケージを使用して開発することができる。Ｓｔａｔｅｆｌｏｗ（Ｒ）は、ザ・マスワークス・インコーポレーテッドの製品である。前記状態モデルのソフトウエアコード表現は、Ａｄａ用のＲａｖｅｎｓｃａｒプロファイル（現在、「ＲａｖｅｎＳＰＡＲＫ」と呼ばれている）などの同時プログラミングの要件に適合することができる自動発生の安全な言語サブセット、又は他の同様な手法を使用して開発することができる。
【００１８】
前記状態モデルの数学的表現は、「Ｃｉｒｃｕｓ」のような自動発生の形式的言語、又は他の同等の形式的言語を使用して開発することができる。「Ｃｉｒｃｕｓ」は、基本的に、２つの別の形式的言語、すなわち、相互通信逐次プロセス系（ＣＳＰ）と「Ｚ」とを組み合わせた言語である。モデルチェッキングは、ＦＤＲ（Failures-Divergence Refinement：障害分散改良）のようなツールを使用して実行することができる。
【００１９】
本発明の更に別の実現形態により、検証ソフトウエアコード生成の方法が提供され、本方法は、
ｉ．要件のステートメントを開発するステップと、
ｉｉ．前記要件のステートメントから状態モデルを生成するためにソフトウエアを使用するステップと、
ｉｉｉ．前記状態モデルから数学的表現で形式的仕様を開発するステップと、
ｉｖ．前記状態モデルを表現するソフトウエアコードを開発するために、前記状態モデルを使用するステップと、
ｖ．検証条件を準備するために、前記数学的表現と前記開発されたソフトウエアコードとを使用して適合引数を構成するステップと、
ｖｉ．前記数学的表現と前記開発されたソフトウエアコードとの間に不一致がある場合に、新たなソフトウエアコードを生成するステップと、
ｖｉｉ．前記新たなソフトウエアコードが、前記数学的表現と前記要件のステートメントとの正確な表現であることを証明するために、前記検証条件を履行するステップとを含んでいる。
上述の方法は、形式的仕様におけるモデルチェッキングを実行する付加的なステップ含んでいる。
【００２０】
本発明は、航空電子工学システムの分野において、とりわけ、高度航空電子工学アーキテクチャ（ＡＡＡ）の実施を通して特に有益であることが分かる。前記ＡＡＡの基本は、共通の機能を個々のシステムから除去することであり、それらは、「プールした」リソース上に実装される。これは、フライト制御、兵器制御、及び（レーダーのような）感知などの種々のシステムが共通リソースを共有することを可能にする。
ＡＡＡシステムには、機能性を維持しながら複数のハードウエア構成要素の故障に対処するために、システムがそれ自体を再設定できるという固有の冗長性がある。
【００２１】
しかしながら、このような固有の冗長性をもたらすＡＡＡの特徴は、下部のソフトウエアを検証することを非常に難しくしている。ＡＡＡ用の主ドライバには、軍用ハードウエア構成要素がない。したがって、市販の在庫部品（ＣＯＴＳ）の構成要素を使用する必要がある。再設定可能な航空電子工学システムに基づくＣＯＴＳを使用するコスト上の利点は、アップグレードが簡単で長期間の利益をもたらすことである。
【００２２】
しかしながら、そのようなシステムを提供するソフトウエアは、その機能性がプラットフォーム（マイクロプロセッサ）独立型であり、できるだけソフトウエアの設計が自動化されて容易に検証可能であるべきである。それはまた、オープンシステム手法を採用するので非常に広く応用することができる。
本発明は、それぞれの事例における仕様に対して検証可能なソフトウエアコードを生成することを目的とする。他の手法には、検証不能という高いリスクがあり、発生した開発コストなどが無駄になる。本発明は、システム設計者が１つのデザインに対して多くの繰返しを行うことを可能にし、各繰返しに対して検証システムを得るのにほんの僅かなコストが必要なだけである。これは、過去において変更するのが極端にコスト高であった、稼働中の安全上重大なソフトウエアに対して特に有効である。
【００２３】
本発明を使用することにより、いかなる変更も自動化されてその結果が検証できるので、比較的単純明快である。これはまた、オペレーション的に非常に長い時間スケールで達成する必要があるアップグレードに対して重要な意味合いがある。これは、例えば戦闘状態にある戦闘機の航空電子工学のような、軍用装置に対するアップグレードの領域に特に当てはまる。しかしながら、本発明はまた、製品リコールに極端に費用がかかる自動車産業のような他の分野でも有益であろう。
【発明を実施するための最良の形態】
【００２４】
ここで、本発明を添付図面を参照して例示的に以下に説明する。
図１に示すように、高度航空電子工学アーキテクチャ（ＡＡＡ）内のソフトウエアは、３つの個別の部分として考えることができる。これらの部分は、破線で示すリアルタイムオペレーティングシステム層（１）、破線で示すアプリケーション層ソフトウエア（２）、及び「ＡＡＡ」制御ソフトウエア（３）を含んでいる。
【００２５】
前記オペレーティングシステム層（１）は、オペレーティングシステム（１ａ）を有する。前記アプリケーション層ソフトウエア（２）は、いくつかの機能的アプリケーション（４）を有する。前記オペレーティングシステム層（１）と、前記アプリケーション層ソフトウエア（２）とは、ＡＡＡ制御ソフトウエア（３）を通じて互いにリンクされ、このＡＡＡ制御ソフトウエア（３）は、アプリケーション層ソフトウエア（２）と協働するアプリケーション管理コード（５）と、オペレーティングシステム層（１）と協働する汎用システム管理ソフトウエア（６）とを有する。これら３つの部分は、全て基板支持層（７）とプロセッサ（８）とによって支持される。
【００２６】
ＡＡＡソフトウエアを検証するために、前記３つの部分は、それぞれ検証されなければならない。ＡＡＡへの鍵は、プラットフォームに依存しないことである。従って、３つの部分は、プロセッサ（８）からできるだけ隔離されることが重要である。前記ＡＡＡ制御ソフトウエア（３）は、必要に応じてリソースの優先権を割り当て、ハードウエアの障害時にはプロセッサに機能性を再割り当てする。それは、一般的な「ｉｆ  ｔｈｅｎ  ｅｌｓｅ」機能であり、予めコード化されたアルゴリズムに従って優先順位を付ける。前記機能はＡＡＡの主要な利点を害することなく分離することができないので、これは、アプリケーション層ソフトウエア（２）を検証することを困難にしている。これにより、ＡＡＡ制御コードソフトウエア及びアプリケーションソフトウエアの検証の達成を本質的に難しくさせている。
【００２７】
公知の方法の図２に示すように、専門のソフトウエアを使用することは、前記開発されたアプリケーション層ソフトウエア（２）のＳｉｍｕｌｉｎｋ（Ｒ）モデル（９）を生成することを可能にしている。このモデルは、ＳＰＡＲＫ  Ａｄａのソフトウエアコード表現（１０）と、Ｓｉｍｕｌｉｎｋ（Ｒ）モデル（９）のＣｌａｗＺの「Ｚ」ファイル形式（１１）における数学的表現とを自動的に生成するために使用され得る。ソフトウエアコード表現（１０）は、ＰｒｏｏｆＰｏｗｅｒ（Ｒ）に適合引数を構成するため、及び（１２）で示されるような検証条件を生成するために、ＣｌａｗＺの「Ｚ」ファイル（１１）と比較される。ＣｌａｗＺの「Ｚ」ファイル（１１）と、ソフトウエアコード表現（１０）とが適合することが検証される場合、前記検証条件は、要求された検証を提供することを履行する（１３）。
【００２８】
本発明の方法の図３は、制御システムの要件を、例えばＳｔａｔｅｆｌｏｗ（Ｒ）などの適切なソフトウエアパッケージに入力することにより、状態モデル（１４）が直接開発されることを示す。次いで、状態モデル（１４）の数学的表現であるＣＳＰ／Ｚファイル（１５）の自動発生用の入力を提供するために、この状態モデル（１４）が使用される。また、この状態モデル（１４）は、ＲａｖｅｎＳＰＡＲＫ  Ａｄａソフトウエア制御コード（１６）の自動発生をもたらすためにも使用される。前記ＣＳＰ／Ｚファイル（１５）とソフトウエア制御コード（１６）とは、（１７）によって示されるような検証条件を発生するＰｒｏｏｆＰｏｗｅｒ（Ｒ）に適合引数を構成するために使用される。ＣＳＰ／Ｚファイル（１５）とソフトウエア制御コード（１６）とが適合することが検証される場合、前記検証条件は、要求された検証ｒ証明を提供することを遂行する（１８）。最後に、（図示しない）モデルチェッキングが、状態関連エラーがあるか否かを表示する。
【００２９】
図４は、フライト制御システム（２１）、兵器制御システム（２２）、及びユーティリティ制御システム（２３）のためのＳｔａｔｅｆｌｏｗ（Ｒ）入力（２０）を生成するため、ＡＡＡ（１９）が使用されることを概略的に示している。フライト制御システム（２１）をＣｌａｗＺファイル（２４）に変換することは容易である。兵器制御システム（２２）及びユーティリティ制御システム（２３）は、Ｓｔａｔｅｆｌｏｗ（Ｒ）の出力（それぞれ２５及び２６）を有するように示されている。
【図面の簡単な説明】
【００３０】
【図１】ソフトウエアに実現された、高度航空電子工学アーキテクチャ（ＡＡＡ）の概略実施例を示す図である。
【図２】検証ソフトウエア制御コードの開発に使用される公知の方法、すなわち従来のＣｌａｗＺに基づく手法を概略的に示す図である。
【図３】検証ソフトウエア制御コードの開発に使用される本発明の方法、すなわち状態に基づくモデリングの使用を概略的に示す図である。
【図４】ＡＡＡに適用されるような本発明のアプリケーションの概要を概略的に示す図である。
【符号の説明】
【００３１】
１４  状態モデル
１５  「ＣＳＰ／Ｚ」ファイル
１６  ソフトウエア制御コード
１７  検証条件
１８  検証条件の履行
【国際公開パンフレット】
2004532487.tif 000002
2004532487.tif 000003
2004532487.tif 000004
2004532487.tif 000005
2004532487.tif 000006
2004532487.tif 000007
2004532487.tif 000008
2004532487.tif 000009
2004532487.tif 000010
2004532487.tif 000011
2004532487.tif 000012
2004532487.tif 000013
2004532487.tif 000014
2004532487.tif 000015
2004532487.tif 000016
【国際公開パンフレット（コレクトバージョン）】
2004532487.tif 000017
【国際調査報告】
2004532487.tif 000018
2004532487.tif 000019
2004532487.tif 000020