(57)【要約】      （修正有）【課題】故障に直面したとき、物理的システムのモデルの堅牢性を検証する方法を提案する。【解決手段】本発明の方法は、１組（１２）のコンポーネント（１２ａ、１２ｂ、１２ｃ）および入力値を挿入するための少なくとも１つの入力インタフェース（１４）を備える物理的システムの第１のモデル（１０）を定義するステップであって、上記第１のモデルは、上記コンポーネントの各々の振る舞いと機能を記述する形式言語で定義されるステップと、物理的システムのモデルによって満足されなければならない決定された属性を形式言語で定義するステップと、第１のモデルに対応し且つ故障投入メカニズムによって強化された第２のモデルを形式言語で定義するステップと、上記決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせを自動的に検索すべく形式試験手段を用いるステップと、を備えている。【選択図】図２
2005353042.tif 000002
【特許請求の範囲】
【請求項１】
物理的システムのモデルの堅牢性を検証する方法であって、
・  １組（１２）のコンポーネント（１２ａ、１２ｂ、１２ｃ）および入力値を挿入するための少なくとも１つの入力インタフェース（１４）を備える物理的システムの第１のモデル（１０）を定義するステップであって、前記第１のモデルは、前記コンポーネントの各々の振る舞いと機能を記述する形式言語で定義されるステップと、
・  物理的システムのモデルによって満足されなければならない決定された属性を形式言語で定義するステップと、
・  第１のモデルに対応し且つ故障投入メカニズム（２２）によって強化された第２のモデル（２０）を形式言語で定義するステップと、
・  前記決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせを自動的に検索すべく形式試験手段を用いるステップと、
の各ステップを備えることを特徴とする、方法。
【請求項２】
故障投入メカニズム（２２）は、故障入力インタフェース（２４）を介して第２のモデル（２０）に少なくとも１つの故障を投入することを含むことを特徴とする、請求項１に記載の方法。
【請求項３】
故障投入メカニズム（２２）は、前記電子的システムのコンポーネントの各々の機能または振る舞いにおける前記少なくとも１つの故障の影響の形式言語での記述をさらに備えることを特徴とする、請求項２に記載の方法。
【請求項４】
決定された属性は、形式試験手段が、前記決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせを見出せないときに、第２のモデル（２０）に対して真であるとみなされることを特徴とする、請求項１に記載の方法。
【請求項５】
物理的システムのモデルは、前記決定された属性に対して堅牢であるとみなされることを特徴とする、請求項４に記載の方法。
【請求項６】
決定された属性は、形式試験手段が、前記決定された属性を欠陥とさせる投入された故障および／または入力値の少なくとも１つの組み合わせを見出すときに、第２のモデル（２０）に対して偽であるとみなされることを特徴とする、請求項１に記載の方法。
【請求項７】
決定された属性を欠陥とさせる投入された故障および／または入力値の前記組み合わせは、訂正されるべき物理的システムのモデルをより堅牢にさせることを可能とし得るシナリオに対応することを特徴とする、請求項６に記載の方法。
【請求項８】
故障の組み合わせは、予め定義された故障の組から選択されることを特徴とする、請求項１から７のいずれか一項に記載の方法。
【請求項９】
決定された属性は、前記物理的システムの状態または振る舞いを記述していることを特徴とする、請求項１から８のいずれか一項に記載の方法。
【請求項１０】
決定された属性は、前記物理的システムの安全性属性であることを特徴とする、請求項９に記載の方法。
【請求項１１】
物理的システムのモデルの堅牢性を検証するシステムであって、
・  物理的システムを定義し、且つ１組（１２）のコンポーネント（１２ａ、１２ｂ、１２ｃ）および入力値を挿入するための少なくとも１つの入力インタフェース（１４）を備える第１のモデル（１０）であって、前記第１のモデルは、前記コンポーネントの各々の振る舞いと機能を記述する形式言語で定義される第１のモデルと、
・  物理的システムのモデルによって満足されなければならない、形式言語で定義された所定の属性と、
・  形式言語で定義された第２のモデル（２０）であって、故障を投入するためのメカニズム（２２）によって強化された第１のモデルに対応する第２のモデルと、
・  前記決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせを自動的に検索するための形式試験手段と、
を備えることを特徴とする、システム。
【請求項１２】
故障を投入するためのメカニズム（２２）は、故障入力インタフェース（２４）と、故障適用手段（２０）とを備えることを特徴とする、請求項１１に記載のシステム。
【請求項１３】
物理的システムは、飛行機エンジンを制御するための２つのコンピュータを備える電子的システムであることを特徴とする、請求項１１または１２に記載のシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、故障（ｐａｎｎｅ、ｆａｌｓｅ）発生に直面しての物理的システムのモデルの堅牢性をチェックする技術の分野に関する。
【背景技術】
【０００２】
航空機または宇宙産業のような、非常に多くの産業において、システムのモデルに依存することは、通常の慣行である。例えば、モデルは、何らかの与えられた使命を達成するために物理的システムから設計され、モデルは、システムとその環境との間の干渉を評価するために使用される。これは、ハードウェア手段かまたはソフトウェア手段かのいずれかを用いてなされる。
【０００３】
特に、故障検出論理、再構成論理、およびコンポーネント冗長は、故障に対するシステム耐性を作るために用いられる。
【０００４】
不幸にして、モデルが、全ての起こり得る事態を考慮に入れることは事実上不可能である。故障の何らかのシーケンスまたは特別な組み合わせが、やはり、システムを停止させ得るように、何らかの特別のシナリオがおろそかにされ、またはシーケンシャル論理エラーが、生じさせられることはしばしば起こる。
【０００５】
それらの問題を解決するために、実際のシステムは、それらの堅牢性を検証するためにベンチテストされる。しかしながら、実際のシステムにおける欠陥を発見するにあたって、主要な新たな工作コスト、ハードウェアおよびソフトウェアリバースエンジニアリング、ならびに時間の主要な損失を包含するシステムを再設計することが必要である。
【発明の開示】
【発明が解決しようとする課題】
【０００６】
本発明の目的は、それゆえ、故障に直面したとき、電子的システムのモデルの堅牢性を検証する方法を提案することによって、上述された問題を解決することである。
【課題を解決するための手段】
【０００７】
このために、本発明は、物理的システムのモデルの堅牢性を検証する方法を提供し、この方法は、
・  １組のコンポーネントおよび入力値を挿入するための少なくとも１つの入力インタフェースを備える物理的システムの第１のモデルを定義するステップであって、上記第１のモデルは、上記コンポーネントの各々の振る舞いと機能を記述する形式言語で定義されるステップと、
・  物理的システムのモデルによって満足されなければならない決定された属性を形式言語で定義するステップと、
・  第１のモデルに対応し且つ故障（ｐａｎｎｅ）投入（ｉｎｊｅｃｔｉｏｎ）メカニズムによって強化された第２のモデルを形式言語で定義するステップと、
・  上記決定された属性を欠陥（ｄｅｆａｕｔ、ｆａｉｌ）とさせる投入された故障および／または入力値の組み合わせを自動的に検索すべく形式試験手段（ｍｏｙｅｎ  ｄｅ  ｐｒｅｕｖｅ  ｆｏｒｍａｌｌｅ）を用いるステップと、
の各ステップを備えることを特徴としている。
【０００８】
したがって、第２のモデルは、物理的システムが、それが故障に直面して堅牢であるように設計され、且つこのために特にシステムを作る前に達成されることを可能として、それゆえそれを開発するコストを低減することを可能とさせる。
【０００９】
この方法は、故障および／またはシステムへの入力値の種々の組み合わせを考慮することによってシステムの属性を検証することを可能とさせる。
【００１０】
また、システムに、いかなる考えられる故障または故障のシーケンスをも徹底的に検証することによって、非常に高い品質および良好な安全性からなるようにさせることも可能とさせる。
【００１１】
本発明の１つの特徴によれば、故障投入メカニズムは、故障入力インタフェースを介して第２のモデルに少なくとも１つの故障を投入するステップを含んでいる。
【００１２】
本発明の他の特徴によれば、故障投入メカニズムは、上記電子的システムのコンポーネントの各々の機能または振る舞いにおける、上記少なくとも１つの故障の影響の形式言語での記述をさらに備えている。
【００１３】
決定された属性は、形式試験手段が、上記決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせを見出せないときに第２のモデルに関して真であるとみなされる。この場合において、物理的システムのモデルは、上記決定された属性に対して堅牢であるとみなされる。
【００１４】
決定された属性は、形式試験手段が、上記決定された属性を欠陥とさせる投入された故障および／または入力値の少なくとも１つの組み合わせを見出すときに、第２のモデルに対して偽であるとみなされる。この場合において、決定された属性を欠陥とさせる投入された故障および／または入力値の上記組み合わせは、訂正されるべき物理的システムのモデルをより堅牢にさせることを可能とし得るシナリオに対応している。
【００１５】
都合良くは、故障の組み合わせは、予め定義された故障の組から選択される。
【００１６】
決定された属性は、上記物理的システムの状態または振る舞いを記述している。それは、上記物理的システムの安全性属性であっても良い。
【００１７】
本発明の方法およびシステムの他の特徴および利点は、限定的でない指摘として与えられ、且つ添付図面を参照してなされる以下の説明を読むことによって、一層明確に表れる。
【発明を実施するための最良の形態】
【００１８】
図１は、物理的システムをモデル化するために使用され得るシステムを示している。システムは、本発明の方法を実施すべく設計されたコンピュータプログラムを実行するために使用されるワークステーションまたはコンピュータ１を備えている。
【００１９】
コンピュータ１は、このタイプの装置に普通に見られるハードウェア手段を備えている。より詳細には、コンピュータは、本発明の方法に従ったプログラムの命令のシーケンスを実行する中央ユニット２と、データおよび実行されるプログラムを格納する中央メモリ３と、使用されているデータおよびプログラムを長期間格納するためのディジタルデータ格納媒体（ハードディスク、コンパクトディスク（ＣＤ）４、フロッピディスク、…）と、入力周辺装置（キーボード５、マウス６、…）と、物理的システムのモデルが見られることを可能とするための出力周辺装置（画面７、プリンタ、…）とを備えている。
【００２０】
本発明に従って、図２は、物理的システムを設計するための第１のモデル１０を示している。例えば、物理的システムは、エンジンを安定化するための設備を監視することまたは制御することのような与えられた応用をサポートするために、以前に作られた電子的システムであっても良い。
【００２１】
第１のモデル１０は、相互間で通信するコンポーネント１２ａ、１２ｂ、１２ｃの１組１２と、入力値を挿入するための少なくとも１つの入力インタフェース１４と、少なくとも１つの出力インタフェース１６とを備えている。当然のこととして、コンポーネントの組１２は、物理的システムの精度または特異性およびモデルに依存する抽象概念のスケールまたはレベルで定義されても良い。
【００２２】
この第１のモデル１０は、作られるべき物理的システムのアーキテクチャを表現する数値モデルである。それは、コンポーネント１２ａ、１２ｂ、および１２ｃの各々の振る舞いおよび機能を記述する、アルファベットまたは変数、論理的量記号、および論理的コネクタを備える「信号」タイプの形式言語で定義される。第１のモデル１０は、従って物理的システムが動的に表現されることを可能としている。
【００２３】
図３は、第１のモデル１０の有効性を決定するための主要なステップ群を示すフローチャートである。
【００２４】
ステップＥ１において、第１のモデルは、形式言語で定義される。
【００２５】
それから、ステップＥ２において、物理的システムのモデルによって満足されなければならない決定された属性も、形式言語で定義される。属性の形式記述は、上記属性に対応する事象を定義すること、およびこの事象を、モデルの変数または信号を基礎として、例えば信号言語でエンコードすることにある。決定された属性は、一般に「そのような事象は決して起きないであろう」タイプの安全性属性であるが、「そのような状態から、時間の有限の長さの最後においてそのような他の状態に達することが可能である」タイプの反応属性であってもよい。この属性は、そのとき第１のモデルの特性を満足しまたは記述しなければならない。
【００２６】
形式言語は、第１のモデル内へ入力されるいかなる値または値の組み合わせに対しても決定された属性の真偽を意味論的に検証するための、ＳＩＬＤＥＸ（商標）ソフトウェアにおける「形式プルーバ」または「チェッカ」のような、形式試験手段を有している。
【００２７】
したがって、ステップＥ３は、入力値のいかなる組み合わせに対しても決定された属性の真偽のテストである。このステップにおいて、この決定された属性を欠陥とさせる入力値の組み合わせについて、形式試験手段によって、自動的な検索がなされる。
【００２８】
もしも形式試験手段が、決定された属性を欠陥とさせる入力値の組み合わせを見つけることができなければ、そのときは、ステップＥ４において、第１のモデル１０は、上記属性に対して有効であるとみなされる。
【００２９】
対照的に、もしも決定された属性が偽（ｆａｕｘ、ｆａｌｓｅ）であるとみなされ、すなわちもしもステップＥ３における形式試験手段が、この決定された属性を欠陥とさせる入力値の少なくとも１つの組み合わせを見つけるならば、そのとき方法は、ステップＥ５に移行する。
【００３０】
ステップＥ５において、診断が提供され、決定された属性を欠陥とさせる入力値のシーケンスを備えている。
【００３１】
ステップＥ６において、前のステップにおいて提供される診断に依存して、第１のモデル１０は、決定された属性が満足されるように訂正されるか、あるいはさもなければ形式試験手段によって見つけられる入力値の組み合わせがほとんどありそうもないことが確認されるかである。
【００３２】
本発明に従って、図４は、物理的システムの第１のモデル１０に対応し、且つ故障投入メカニズム２２によって強化された第２の数値モデル２０の、高度に概略的な図である。
【００３３】
第２のモデル２０は、コンポーネント１２ａ、１２ｂ、および１２ｃの１組１２と、入力および出力インタフェース１４および１６とに加えて、それを介して少なくとも１つの故障または故障の組み合わせが投入される故障入力インタフェース２４を、故障適用手段２６と共に備える、故障投入メカニズム２２をさらに備えることにおいて、第１のモデル１０と異なっている。
【００３４】
故障または故障の組み合わせは、１組の予め定義された故障から選択される。第２のモデル２０の振る舞いにおける各故障の影響は、形式言語によってモデル化され、そして与えられたコンポーネントにおける故障の結果は、上記コンポーネントについての振る舞い図表に記述される。第２のモデル２０の最小のコンポーネントにおける全ての既知の可能性のある故障が、リストされ、且つ従って、例えば、ワークステーションまたはコンピュータ１の中央メモリ３に格納されるデータベースにおける各コンポーネントの振る舞い図表に配置される。
【００３５】
換言すれば、故障投入メカニズム２２は、物理的システムをモデル化する第２のモデル２０のコンポーネント１２ａ、１２ｂ、１２ｃの各々の機能または振る舞いにおける、いかなる故障の影響の形式言語での記述をも含んでいる。
【００３６】
したがって、第２のモデル２０は、予見できる故障に関連して存在するのと同じくらい多くの、付加的なブール入力およびプロセスに増大された第１のモデル１０に対応する。そのとき、１つの特定の故障の入力は、「偽」または「真」の２つの値のうちの一方をとり得る。例えば、値「偽」は、状態「故障投入がない」に対応し得るとともに、値「真」は、状態「故障投入がある」に対応し得る。
【００３７】
故障入力インタフェース２４の入力の全てが、偽であるとき、第２のモデル２０は、そのとき公称条件のもとで動作する。故障入力が真であるとき、それは、そのコンポーネントについての振る舞い図表の適用に関するコンポーネントに故障を適用するための論理をトリガする。
【００３８】
加えて、故障入力が開放されているとき、形式試験手段は、決定された属性を欠陥とさせ得る故障および／または入力値のシーケンスまたは組み合わせを探すために、故障をいつでも導入することができる。
【００３９】
形式試験手段は、それが決定された属性を記述する式を得るまで、第２のモデル２０のコンポーネント１２ａ、１２ｂ、および１２ｃについての原理および／または振る舞い図表に論理ルールを適用するツールである。
【００４０】
この形式試験ツールは、シミュレーションの間の全ての瞬間において、故障投入メカニズム２２を介して第２のモデル２０のコンポーネントまたは機能に故障を適用し得るＳＩＬＤＥＸ（商標）タイプのソフトウェアによって提供され得る。
【００４１】
特に、第２のモデル２０の決定された属性を試験するために、ＳＩＬＤＥＸ（商標）タイプの形式言語における動的コンパイルが起動される。もしも、コンパイルが成功すれば、そのときは、決定された属性が有効とされる。さもなければ、形式試験手段は、システムが上記属性を否定する状態をとってモデル化されるように導く故障および／または入力値のシーケンスを含むシナリオを与える。
【００４２】
図５は、故障の発生に直面して物理的システムのモデルの堅牢性を検証するための主要なステップ群を図解するフローチャートである。
【００４３】
ステップＥ１１において、第２のモデル２０は、故障投入メカニズム２２によって強化された第１のモデル１０に対応する形式言語で定義される。
【００４４】
その後は、図２のフローチャートのステップＥ２で定義され、且つ第１のモデル１０について真であるとして既に検証されている（ステップＥ４）決定された属性が、第２のモデル２０についても依然として真であるかどうかが検証される。
【００４５】
ステップＥ１３の間に、決定された属性の真偽が、投入された故障および／または入力値のいかなる組み合わせについてもテストされる。このステップの間に、上記決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせについて、形式試験手段によって、自動的な検索がなされる。
【００４６】
もしも、形式試験手段が、上記決定された属性を欠陥とさせる投入された故障および／または入力値のいかなる組み合わせも見つけることができないならば、そのときは属性は真であるとみなされ、そしてその結果として、ステップＥ１４において、物理的システムのモデルは、決定された属性に関連する故障に直面して堅牢であるとみなされる。
【００４７】
対照的に、もしもステップＥ１３の間に、形式試験手段が、上記決定された属性を欠陥とさせる投入された故障および／または入力値の少なくとも１つの組み合わせを見つけるならば、そのときは、上記属性は偽であるとみなされ、そしてその結果として、ステップＥ１５において、形式試験手段によって診断が提供される。この診断は、所望されていない状況に導く故障および入力値２４および１４を介しての入力のシナリオまたはシーケンスを備えている。
【００４８】
ステップＥ１６において、診断は分析され、すなわち第２のモデル２０における動作のシーケンスが、故障または各故障が投入される瞬間であるとして検査される。この分析は、物理的システムのモデルの設計を見直させ、またはこれに反して形式試験手段によって見つけられたシナリオがありそうもないことを確認させる。
【００４９】
図６から図８は、物理的システムのモデルの堅牢性を検証する単純化された例を示している。
【００５０】
この例において、設計されるものである物理的システムは、飛行機エンジンを制御するために、２つのコンピュータを備える電子的システムである。通常の操作において、ただ１つのコンピュータがエンジンを制御し、且つ２つのコンピュータの間に対話またはデータの交換が生じる。したがって、１つのコンピュータが故障した場合には、第２のコンピュータが単一コンピュータモードでの実行を開始させなければならない。この例において、システムの損失は、両方のコンピュータが同時に故障しており、または受動的であり、または能動的であることに対応する。
【００５１】
したがって、図６は、第１の入力インタフェース１１４ａおよび第１の出力インタフェース１１６ａを有する第１のコンピュータ１１２ａと、第２の入力インタフェース１１４ｂおよび第２の出力インタフェース１１６ｂを有する第２のコンピュータ１１２ｂと、第１と第２のコンピュータ１１２ａと１１２ｂの間における対話またはデータの交換を可能とする接続ワイアを有するコンピュータ間ハーネス１１２ｃとをモデル化する、物理的システムの第１のモデル１１０の例を示している。矢印Ｆ１は、第１のコンピュータ１１２ａによって第２のコンピュータ１１２ｂへ送信される信号またはデータ（信号言語でＳ＿１＿２と書かれる）を指し示し、矢印Ｆ２は、第２のコンピュータ１１２ｂから第１のコンピュータ１１２ａへ行く信号またはデータ（信号言語でＳ＿２＿１と書かれる）を表している。
【００５２】
図７は、図６の第１のモデル１１０に対応し、且つ故障入力インタフェース１２４および故障適用手段１２６を備える故障投入メカニズム１２２によって強化された、物理的システムの第２のモデル１２０を示している。この例において、故障適用手段１２６は、開回路となる単一の接続ワイア、または短絡回路とされるワイア、または接続されないハーネス１１２ｃにおける故障をシミュレートするスイッチ手段を備えている。矢印Ｆ１ａは、第１のコンピュータ１１２ａを出る信号Ｓ＿１＿２を表し、そして、矢印Ｆ１ｂは、故障適用手段１２６を通過した後に第２のコンピュータ１１２ｂに入る信号Ｓ＿２＿１＿ｖを表す。矢印Ｆ２ｂは、第２のコンピュータ１１２ｂを出る信号Ｓ＿２＿１を指示し、そして、矢印Ｆ２ａは、故障適用手段１２６を通過した後に第１のコンピュータ１１２ａに入る信号Ｓ＿１＿２＿ｖを表す。故障がないときは、第１または第２のコンピュータ１１２ａまたは１１２ｂを出る信号は、それぞれ、変化されずに第２または第１のコンピュータ１１２ｂまたは１１２ａに入る。対照的に、故障の場合には、コンピュータ１１２ａ、１１２ｂの一方または他方を出る信号はその送り先に到達しない。信号言語において、このことは次の式で表現される。
Ｓ＿１＿２＿ｖ  ＝  Ｓ＿１＿２  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
Ｓ＿２＿１＿ｖ  ＝  Ｓ＿２＿１  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
【００５３】
図８は、図７の故障投入メカニズムおよび特に故障適用手段１２６を示す高度に概略的な図である。故障適用手段１２６は、「ハーネスが接続されていない」に対応する第１の故障入力１２４ａと、「対話ワイアが中断された」に対応する第２の故障入力１２４ｂとを備えている。第１および第２の故障入力１２４ａおよび１２４ｂは、第１のコンピュータ１１２ａから第２のコンピュータ１１２ｂへデータを転送するかまたは転送しないための第１の結合／切り離し手段１３４に、ならびに第２のコンピュータ１１２ｂから第１のコンピュータ１１２ａへデータを転送するかしないかするための第２の結合／切り離し手段１３６にその出力が印加される、論理オア（ＯＲ）ゲート１３２の入力に結合されている。
【００５４】
故障入力は、モデル化されたコンポーネントに故障を適用するためのボタンとみなされ得る。したがって、シミュレーションの間、所望の瞬間に故障を導入することが可能である。
【００５５】
形式試験手段が、決定された属性を欠陥とさせる投入された故障および／または入力値の組み合わせの自動的な検索に取りかかっているとき、「偽」値に設定される入力は、反例シナリオの検索に含まれない。自由入力のみがこの検索に含まれる。
【００５６】
したがって、第１の結合手段１３４に故障が何も投入されないとき、入力信号ＳＡ＿ｅ、ＳＢ＿ｅ、ＳＣ＿ｅ、およびＳＤ＿ｅは、それぞれ結合手段１３４の出力信号ＳＡ＿ｓ、ＳＢ＿ｓ、ＳＣ＿ｓ、およびＳＤ＿ｓと等しい。そのような状況のもとで、第１のコンピュータ１１２ａから送信される信号ＳＡ＿１＿２、ＳＢ＿１＿２、ＳＣ＿１＿２、およびＳＤ＿１＿２は、第１の結合手段１３４によって有効とされ、そして第２のコンピュータに送られ、それぞれ次のように記述される。ＳＡ＿１＿２＿ｖ、ＳＢ＿１＿２＿ｖ、ＳＣ＿１＿２＿ｖ、およびＳＤ＿１＿２＿ｖ。
【００５７】
同様にして、第２の結合手段１３６に故障が何も投入されないとき、入力信号ＳＥ＿ｅ、ＳＦ＿ｅ、ＳＧ＿ｅ、およびＳＨ＿ｅは、それぞれ結合手段からの出力信号ＳＥ＿ｓ、ＳＦ＿ｓ、ＳＧ＿ｓ、およびＳＨ＿ｓに等しい。そのような状況のもとで、第１のコンピュータ１１２ｂから送信される信号ＳＥ＿１＿２、ＳＦ＿１＿２、ＳＧ＿１＿２、およびＳＨ＿１＿２は、それぞれ次のように第１のコンピュータ１１２ａに送られるべく第２の結合手段１３６によって有効とされる。ＳＥ＿１＿２＿ｖ、ＳＦ＿１＿２＿ｖ、ＳＧ＿１＿２＿ｖ、およびＳＨ＿１＿２＿ｖ。
【００５８】
「ハーネスが接続されていない」に対応する第１の故障入力１２４ａおよび／または「対話ワイアが中断された」に対応する第２の故障入力１２４ｂが、接続されていないとき、形式試験手段またはプルーバは、いつでもハーネス切断および／またはワイア切断を導入し得る。そのような状況のもとで、コンピュータ１１２ａ、１１２ｂの１つによって送信される信号は、他のコンピュータに到達しない。
【００５９】
初期化の後、上述の例は、信号言語にて次のように記述され得る。
Ｐｒｏｃｅｓｓ  ｘｘｘ＿ｐｒｏｃｅｓｓ＿ｓｉｌｄｅｘ＿１＝
（？  ｂｏｏｌｅａｎ  ＳＡ＿ｅ，ｆａｕｌｔ，ＳＢ＿ｅ，ＳＣ＿ｅ，ＳＤ＿ｅ；
｜  ｂｏｏｌｅａｎ  ＳＡ＿ｓ，ＳＢ＿ｓ，ＳＣ＿ｓ，ＳＤ＿ｓ；）
（｜  （｜  ＳＡ＿ｓ  ＝  ＳＡ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ  
｜  ＳＢ＿ｓ  ＝  ＳＢ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ＳＣ＿ｓ  ＝  ＳＣ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ＳＤ＿ｓ  ＝  ＳＤ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ｆａｕｌｔ＾＝  ＳＡ＿ｅ＾＝  ＳＢ＿ｅ＾＝  ＳＣ＿ｅ＾＝  ＳＤ＿ｅ  
｜）
｜）；
ｐｒｏｃｅｓｓ  ｘｘｘ＿ｐｒｏｃｅｓｓ＿ｓｉｌｄｅｘ＿２＝
（？  ｂｏｏｌｅａｎ  ＳＥ＿ｅ，ｆａｕｌｔ，ＳＦ＿ｅ，ＳＧ＿ｅ，ＳＨ＿ｅ；
｜  ｂｏｏｌｅａｎ  ＳＥ＿ｓ，ＳＦ＿ｓ，ＳＧ＿ｓ，ＳＨ＿ｓ；）
（｜  （｜  ＳＥ＿ｓ  ＝  ＳＥ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ＳＦ＿ｓ  ＝  ＳＦ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ＳＧ＿ｓ  ＝  ＳＧ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ＳＨ＿ｓ  ＝  ＳＨ＿ｅ  ｗｈｅｎ  ｎｏｔ  ｆａｕｌｔ
｜  ｆａｕｌｔ＾＝  ＳＥ＿ｅ＾＝  ＳＦ＿ｅ＾＝  ＳＧ＿ｅ＾＝  ＳＨ＿ｅ
｜）
｜）；
【００６０】
一般に、２つのコンピュータを有する物理システムのモデルにおいて、次の２つの属性を検査することができる。「システムのモデルは、それ自体で２つのコンピュータがアクティブであると見出せない」および「システムのモデルは、それ自体で２つのコンピュータがパッシブであると見出せない」。
【００６１】
加えて、システムがスイッチオンされたとき、単一の故障が存在する状況をモデル化することを予見することができる。そのような状況のもとで、スイッチオン時に、システムに上述で明記された属性をとらせないかもしれない、何らかの単一の故障が存在するかどうかを検証することができる。
【００６２】
さらにまた、両コンピュータが同時に起動して、動作における単一の故障の存在をモデル化することを予見することができる。そのような状況のもとで、各単一の故障が、いかなる瞬間においても導入され得ると仮定される。このようにするために、問題の故障入力が、全ての他の故障を維持している間に、開放されたままにされ得る。
【００６３】
故障は、次の故障を有する１組の予め定義された故障から選択され得る。故障なし；自動テスト故障；開回路；短絡回路；送信における障害；接続されていないハーネス；同期故障；偽とされるＮＶＭ（不揮発性メモリ）故障；真とされるＮＶＭ故障；偽とされるＰＰＡＶＭ信号故障；真とされるＰＰＡＶＭ信号故障；ＰＰＡＶＭＴＰＢ；コンピュータ故障；偽とされるＰＨ信号故障；真とされるＰＨ信号故障；その他。
【００６４】
したがって、本発明は、物理的システムを作るのに先立って、故障に直面してモデルの堅牢性を検証することを可能とさせ、それによって作られるべきシステムが、システムの開発のコストを低減しつつ良好な安全性を呈することを可能としている。
【００６５】
もちろん、本発明は、既に作られている物理的システムの堅牢性を検証することをも可能とさせる。そのような状況のもとで、物理的システムは、形式言語におけるモデルを用いてモデル化され、且つ物理的システムのモデルの堅牢性が、故障に直面したときにシステムについての決定された属性によって定義される基準に対して、上述されるようにしてチェックされる。
【図面の簡単な説明】
【００６６】
【図１】本発明の方法またはシステムにおいて実施されるハードウェア手段の斜視図である。
【図２】本発明に従って物理的システムを設計するための第１のモデルの高度に概略的な図である。
【図３】図２に示される第１のモデルの有効性を決定するための主要なステップ群を示すフローチャートである。
【図４】本発明に従って故障を投入するためのメカニズムによって強化された、物理的システムの第１のモデルに対応する第２のモデルを示す、高度に概略的な図である。
【図５】本発明に従って、故障の発生に直面した物理的システムのモデルの堅牢性を検証するための主要なステップ群を示すフローチャートである。
【図６】本発明に従って、第１のコンピュータ、第２のコンピュータ、およびハーネスをモデル化する電子的システムの第１のモデルの一例の高度に概略的な図である。
【図７】故障投入メカニズムによって強化された、図６の第１のモデルに対応する第２のモデルを示す高度に概略的な図である。
【図８】故障を投入するための図７のメカニズムの高度に概略的な図である。
【符号の説明】
【００６７】
１  コンピュータ
２  中央ユニット
３  中央メモリ
４  コンパクトディスク（ＣＤ）
５  キーボード
６  マウス
７  画面
１０、１１０  第１のモデル
１２  コンポーネントの組
１２ａ、１２ｂ、１２ｃ  コンポーネント
１４  入力インタフェース
１６  出力インタフェース
２０、１２０  第２のモデル
２２  故障投入メカニズム
１１２ａ、１１２ｂ  第１、第２のコンピュータ
１１２ｃ  コンピュータ間ハーネス
１１４ａ、１１４ｂ  第１、第２の入力インタフェース
１１６ａ、１１６ｂ  第１、第２の出力インタフェース
２４、１２４  故障入力インタフェース
２６、１２６  故障適用手段
１３２  論理オア（ＯＲ）ゲート
１３４  第１の結合／切り離し手段
１３６  第２の結合／切り離し手段
【図１】
2005353042.tif 000003
【図２】
2005353042.tif 000004
【図３】
2005353042.tif 000005
【図４】
2005353042.tif 000006
【図５】
2005353042.tif 000007
【図６】
2005353042.tif 000008
【図７】
2005353042.tif 000009
【図８】
2005353042.tif 000010
【外国語明細書】
2005353042.tif 000011
2005353042.tif 000012
2005353042.tif 000013
2005353042.tif 000014
2005353042.tif 000015
2005353042.tif 000016
2005353042.tif 000017
2005353042.tif 000018
2005353042.tif 000019
2005353042.tif 000020
2005353042.tif 000021
2005353042.tif 000022
2005353042.tif 000023
2005353042.tif 000024
2005353042.tif 000025
2005353042.tif 000026
2005353042.tif 000027
2005353042.tif 000028
2005353042.tif 000029
2005353042.tif 000030
2005353042.tif 000031
2005353042.tif 000032
2005353042.tif 000033
2005353042.tif 000034
2005353042.tif 000035
2005353042.tif 000036