【誤訳訂正書】
【提出日】平成23年1月5日(2011.1.5)
【誤訳訂正１】
【訂正対象書類名】特許請求の範囲
【訂正対象項目名】全文
【訂正方法】変更
【訂正の内容】
【特許請求の範囲】
【請求項１】
組み込まれた電気的システムによってインプリメントされたサービスのための実証環境を設計する方法であって、
前記サービスの１つ以上のユーザ要求およびシステム応答と、前記サービスの前記ユーザ要求および前記システム応答の許されたシーケンスを設定する動作に関するオートマトンとの指定がコンピュータに入力されるステップと、
コンピュータが、シミュレーションツール上の検査環境のモデルのテンプレートである、スケルトン実証環境（図４）を、入力された前記指定のインスタンス化によって自動的に生成し、生成した前記スケルトン実証環境を読み出し可能なメモリデバイスに記憶するステップと、
を含み、前記スケルトン実証環境は、
前記サービスのための初期条件のモデル（４１３または４１５）と、前記サービスのユーザ要求のモデル（４１３または４１５）と、
前記サービスのシステム応答が的確であれば「真」を出力し、前記サービスのシステム応答が的確でないならば「偽」を出力する、システム応答精度のモデル（４１９、４２１）と、
前記動作に関するオートマトンのトラバーサルから生成されてユーザ要求およびシステム応答の許されたシーケンスを網羅する検査オートマトン（４０１）と、
検査環境を表し、全体のシステムが自己完結であるようにするための環境ループ（４１１）と、
を含み、さらに、
前記サービスのシステム応答を前記システム応答精度のモデルの入力とするデータフロー（４５１、４５３）と、
前記システム応答精度のモデルの出力を前記環境ループの入力とするデータフロー（４６１、４６３）と、
前記環境ループの出力を前記ユーザ要求のモデルの入力とするデータフロー（４３１、４３３）と、
前記ユーザ要求のモデルの出力を前記サービスのユーザ要求とするデータフロー（４４１、４４３）と、
前記検査オートマトンから前記ユーザ要求のモデルと前記システム応答精度のモデルの両方にトリガーを与える、制御フロー(４７１)と、
を含むことを特徴とする方法。
【請求項２】
前記スケルトン実証環境に対して、各前記ユーザ要求をソフトウェアで実現する検査要求のファンクションがコンピュータ上に実装されており、各前記システム応答をソフトウェアで実現する１つ以上の状態検査ファンクションがコンピュータ上に実装されていて、コンピュータが、前記スケルトン実証環境のデータフローを、前記検査要求および前記状態検査ファンクションを用いて作成する請求項１記載の方法。
【請求項３】
前記組み込まれた電気的システムをブラックボックスとして、前記サービスをソフトウェアで実現する少なくとも１つのファンクションがコンピュータ上に実装されており、当該少なくとも１つのファンクションの入力および出力が前記サービスのブラックボックス  インターフェースであるとの指定が、コンピュータに入力されていることによって、コンピュータが、前記ブラックボックスの出力を前記状態検査ファンクションの入力に接続し、前記検査要求の出力を前記ブラックボックスの入力に接続し、前記初期条件のモデルと、前記検査要求と、前記状態検査ファンクションとからなる、前記スケルトン実証環境のスケルトンと、実証結果を生成するためのシミュレーション環境でのサービス仕様とを、前記ブラックボックスと接続したスケルトン実証環境における検査結果に応じて修正し、完成するためのスケルトン実証環境を設計者に供するために読み出し可能なメモリデバイスに記憶する請求項２記載の方法。
【請求項４】
前記サービスのためのスケルトン実証環境（ブロック４１７を除く図４）と、同時に、前記ブラックボックスと接続したスケルトン実証環境における検査結果から設計者によって実証された前記サービス（４１７）のモデルとを含む、実証されたモデル（図４）をコンピュータが出力する請求項３記載の方法。
【請求項５】
前記組み込まれた電気的システムの機能が、コンピュータ上にソフトウェア（４１７）で実装されている請求項１乃至４のいずれか１項に記載の方法。
【請求項６】
前記組み込まれた電気的システムの機能が、コンピュータ上のソフトウェアおよびハードウェア（４１７）で実装されており、前記ハードウェアと接続される検査プラットフォーム上に前記スケルトン実証環境が組み込まれている請求項１乃至５のいずれか１項に記載の方法。
【請求項７】
乗物のブレーキ・バイ・ワイヤシステムのような、フォールト・トレラント・システムにおける、複数の同一の前記ユーザ要求のモデルまたは複数の同一の前記検査要求に、コンピュータがフォールト（図１０Ｃ）の投入をする請求項１乃至６のいずれか１項に記載の方法。
【請求項８】
少なくとも１つのユーザ要求を共有する複数のサービスのためのスケルトン実証環境の指定がコンピュータに入力され、前記複数のサービスの組のための統一された実証環境を生成するために、前記サービスの前記スケルトン実証環境をコンピュータが統合することを含む請求項１乃至７のいずれか１項に記載の方法。
【請求項９】
コンピュータに請求項１乃至８のいずれか１項に記載の方法の自動化されたステップのすべてを実行させるためのコンピュータプログラム。
【請求項１０】
コンピュータの読み出し可能な媒体上に記憶された請求項９に記載のコンピュータプログラム。
【誤訳訂正２】
【訂正対象書類名】明細書
【訂正対象項目名】００１３
【訂正方法】変更
【訂正の内容】
【００１３】
したがって、本発明は、組み込まれた電気的システムによって実装されるサービスのための実証環境を設計する方法を提供し、該方法は、
ａ）前記サービスに、１つ以上のユーザ要求およびシステム応答を割り当て、
ｂ）前記サービスに、動作に関するオートマトンを割り当て、前記動作に関するオートマトンは、前記ユーザ要求およびシステム応答の許されたシーケンスを決定し、
ｃ）シミュレーションツール上で実行可能なモデルの形で、前記サービスのためのスケルトン実証環境を自動的に生成し、前記スケルトン実証環境は、前記動作に関するオートマトンのトラバーサルから生じた検査オートマトン、初期状態のモデル、ユーザ要求のモデル、システム応答精度のモデル、環境モデルおよびこれらのモデルをいっしょに集めるデータフローおよび制御フローを含み、前記スケルトン実証環境は、前記サービスのすべてのユーザ要求および結果として生じるシステム応答をカバーし、および
ｄ）設計実証ツールによる使用のためのコンピュータの読み出し可能なメモリデバイスに前記スケルトン実証環境を記録する。
【誤訳訂正３】
【訂正対象書類名】明細書
【訂正対象項目名】００１４
【訂正方法】変更
【訂正の内容】
【００１４】
スケルトンを用いることにより、検査環境とモデルそれ自体の両方を実証するために、検査環境は、検査中のサービスのモデルといっしょにシミュレートすることができる。設計プロセスにおける非常に初期の誤りを修正することにより、本発明の方法は、システム設計と開発において時間の節約を与え、検査範囲と質も非常に改善する。前記サービスは、例えばブレーキ・バイ・ワイヤ等の安全クリティカルおよび／またはフォールトトレラントシステムのような、車両に使用されるサービスを含むことができる。
【誤訳訂正４】
【訂正対象書類名】明細書
【訂正対象項目名】００１６
【訂正方法】変更
【訂正の内容】
【００１６】
ユーザ要求とシステム応答精度のモデルは、以前に開発されたスケルトン実証環境の少なくとも一部を記憶することによって、あらかじめ定義できることは正しく理解されるだろう。
【誤訳訂正５】
【訂正対象書類名】明細書
【訂正対象項目名】００１７
【訂正方法】変更
【訂正の内容】
【００１７】
その方法は、それを実行する１つのファンクションを各ユーザ要求に割り当て、それを実行する１つまたはそれ以上のファンクションを各システム応答に割り当てることを含むことができ、前記スケルトン実証環境のデータフローは、ユーザ要求とシステム応答の前記ファンクションを用いて形成される。
【誤訳訂正６】
【訂正対象書類名】明細書
【訂正対象項目名】００１８
【訂正方法】変更
【訂正の内容】
【００１８】
その方法は、その入力と出力がそのサービスを実行するファンクションの少なくとも１つの入力と出力に対応する、ブラックボックスインターフェースを前記サービスに割り当て、前記サービスブラックボックスの出力を前記スケルトン入力に、前記スケルトン出力を前記サービス・ブラックボックスの入力にインターフェースし、実証の結果を出すために、シミュレーション環境におけるスケルトンとサービス仕様を全部揃え集めることを含むことができる。
【誤訳訂正７】
【訂正対象書類名】明細書
【訂正対象項目名】００２８
【訂正方法】変更
【訂正の内容】
【００２８】
本発明は添付の図面を参照して実施例のみによって述べられる。 
図１は１つのサービスのユースケースの仕様を示す。
図２は１つのサービスの機能的な説明を示す。
図３は１つのサービスの動作に関する記述を示す。
図４は本発明によって自動的に生成される検査環境のスケルトンを示す。
図５は図４における検査環境の一部である検査オートマトンを示す。
図６は１つのサービスの機能的な記述を示す。
図７は２つのＥＣＵと１つのネットワークを含む分配されたシステムを示す。
図８は３つのＥＣＵと１つの配線ネットワークを含む分配されたシステムを示す。
図９はコネクタインターフェースを示す。
図１０は電気的レベルでのフォールトのモデル化を示す。
図１１は本発明による設計プロセスの１つの実施例を示す。
図１２は安全クリティカルシステムの設計プロセスの使用を示す。
図１３はハードウェア  イン  ザ  ループの検査環境を示す。
図１４は例えばＣＡＮバスのようなローカルエリアネットワークにおけるフレームの１つの異なる仕様の完成を示す。
図１５はイン  ザ  ループ  シミュレーションと検査の一般的なパラダイムを示す。
そして、図１６はいくつかの組み合わされたサービスの検査環境の混合を示す。
【誤訳訂正８】
【訂正対象書類名】明細書
【訂正対象項目名】００３３
【訂正方法】変更
【訂正の内容】
【００３３】
我々はまだ、検査ベクトルを生じることからなる通常のアプローチに言及していない。実際、この方法は、適切な検査を生み出すことが困難なので、「イン  ザ  ループ」環境の提示より劣る。本発明のアプローチは、現在に至るまで何の方法も与えられず、イン  ザ  ループの検査の設計は低コストでモデルを作るので、非常にうまくいく。検査環境スケルトンを産出することによって、我々は非常に低コストでこの大発見を与える。実際、モデル  イン  ザ  ループが論文において述べられるとき、対話方式の環境モデルが設計される方法は、決して特定されず、そのシステムの設計者の義務である。図１５に示されるように概略のアイデアは非常にシンプルである。検査中のモデル１５０１と環境モデル１５０３があり、それらはフロー１５１１と１５１３を通して情報のフローを交換する。そのシミュレーションは、そのシステムのモデルにおいて信頼の獲得を促進する。実際には、もし我々が定常的シミュレーションよりほかの何かを、そして我々の発明で提案したような自動の生成の不在において検査したいならば、そのようなモデルの設計は、非常に難しい。例えばブレーキシステムを検査するために、たくさんの場面を考慮に入れなければならない。そのサービスのモデルを実証するためにあとで適用できる、環境を検査するような最小の努力で生成を促進するために、このことが我々の発明の目的であり、そのソフトウェアがそのサービスおよびそのシステムの部分または全体を実行する。
【誤訳訂正９】
【訂正対象書類名】明細書
【訂正対象項目名】００３６
【訂正方法】変更
【訂正の内容】
【００３６】
これが行われたとき、１つのスケルトン実証環境は、そのサービスのために自動的に生成され、そのスケルトン実証環境は、前記動作に関するオートマトンのトラバースから生み出される検査オートマトン、初期条件のモデル、ユーザ要求のモデル、システム応答精度のモデル、環境モデル、およびこれらのモデルを纏めるデータフローおよび制御フローを含む。スケルトン実証環境は、そのサービスのすべてのユーザ要求と結果として生じるシステム応答をカバーする。スケルトン実証環境は図４に示され、そこには検査環境の一般的なフレームワークもまた示される。このフレームワークの特別な例は、このステップで自動的に発生されるスケルトンである。
【誤訳訂正１０】
【訂正対象書類名】明細書
【訂正対象項目名】００３８
【訂正方法】変更
【訂正の内容】
【００３８】
さらに本発明の側面は、各ユーザ要求に、それを実行する１つのファンクションを割り当て、また、各システム応答に、それを実行する１つまたはそれ以上のファンクションを割り当てることを含む。このスケルトン実証環境のデータフローは、図２に関連して述べられるように、ユーザ要求とシステム応答のこれらのファンクションを用いて形成することができる。そのファンクションのデータフローおよび１つのサービスのデータフローの記述が、そのスケルトン実証環境のためのデータフローにいかに変えるかが図４に示される。
【誤訳訂正１１】
【訂正対象書類名】明細書
【訂正対象項目名】００３９
【訂正方法】変更
【訂正の内容】
【００３９】
本発明のさらなる側面は、以下のものを含む。 
ｇ）サービスにブラックボックスインターフェースを割り当てることを含み、その入力と出力はそのサービスを実行するファンクションの少なくとも１つの入力と出力に対応し、
ｈ）そのサービス・ブラックボックスの出力をスケルトン入力に、スケルトン出力をサービス・ブラックボックスの入力にインターフェースし、そして、
ｉ）実証結果を生成するために、シミュレーション環境においてスケルトンおよびサービス仕様を完成し調整（correct）する。
【誤訳訂正１２】
【訂正対象書類名】明細書
【訂正対象項目名】００４５
【訂正方法】変更
【訂正の内容】
【００４５】
図１においては、３つのユースケースの限定されない実施例が示される。これらの好例となるユースケースは、車両のドアの施錠管理の説明の形態で、限定されないサービスの話をする。各ユースケースのために、４つのパートにおける説明がなされる。第１のパート１０１、１１１、１２１は、それぞれのユースケースにおいて適用できるコンテキストである。第２のパート１０３、１１３、１２３は、それぞれのユースケースを述べるユーザ要求である。第３のパート１０５、１１５、１２５は、ユーザ要求によって誘発されるシステム応答である。第４のパート１３１、１３３、１３５は、ユーザ要求とシステム応答との間の呼び出し時間である。それらは最初のステージでは必須ではない。
【誤訳訂正１３】
【訂正対象書類名】明細書
【訂正対象項目名】００４７
【訂正方法】変更
【訂正の内容】
【００４７】
ユースケースのためにたくさんの異なる初期状態を許容するため、コンテキストは多少不明瞭である。例えばドア施錠サービスのためのコンテキストは、すべてのドアが解錠されていることと、エンジンが動いていることでよいかもしれない。
【誤訳訂正１４】
【訂正対象書類名】明細書
【訂正対象項目名】００４８
【訂正方法】変更
【訂正の内容】
【００４８】
システム応答が状態（state）でありユーザ要求が遷移（transition）であることを考慮すると、ユースケース（Use Case）の１セットは、ムーア（Moore）のオートマトンへ変えることができる。正確なプロセスは、そのユースケースのコンテキストに合う初期状態から、そのユースケースのシステム応答に対応する１つの最終の状態へ、遷移の１セットをユースケースに関係づけることにある。サービスの動作に関する説明を得るため、システムの初期状態を特定することが必要である。しかしながら、我々の発明は、ムーアのオートマトンのように動作を特定することができる限り、また、次の図面で示される他の制限の元では、種々の特定するプロセスをサポートする。
【誤訳訂正１５】
【訂正対象書類名】明細書
【訂正対象項目名】００５０
【訂正方法】変更
【訂正の内容】
【００５０】
図３に、ムーアオートマトンのサンプルが示される。状態３２１、３２３、３２５、３２７、３４１、３４３、３４５、３４７および３４９が、数あるなかで遷移３３１、３３３、３３５、３３７、３３９を介して互いにリンクされている。このオートマトンのセマンティックを例によって説明する。例えばドア施錠サービスの例を継続して、状態３４３においては車両が施錠され、状態３４１においては車両が解錠されていることを想定する。それから遷移３３７の間は、解錠の要求がトリガーされることを想定する。図２に概略が示されたスキームに従うと、遷移３３７は刺激２２３によってトリガーすることができ、結果として生じる状態３４１はファンクション２４３をトリガーすることができる。ユースケースとのリンクについては、状態３４１は応答状態１０５および遷移３３７がユーザ要求１０３と対応することできるような結果として生じることができる。それから、状態３４３は初期状態１０１と合わなければならない。
【誤訳訂正１６】
【訂正対象書類名】明細書
【訂正対象項目名】００７６
【訂正方法】変更
【訂正の内容】
【００７６】
図４に描かれたように検査環境または実証環境のインスタンスは、一旦、サービスがブロック４１７において特定されると、自動的に生成することができる。この全く最初のインスタンスは、スケルトン実証環境と呼ばれる。そのスケルトンにおいては、ブロック４１１、４１３、４１５、４１７、４１９および同様のものすべては、自動的に生成される。ブロック間のデータフローは、図４の描写に応じて自動的に生成される。これらのブロックの内部のデータフローもまた自動的に生成され、ブロックは入力もまた出力であるとき、単位元のごとくふるまう。他の入力はそのブロック内で終結する。
【誤訳訂正１７】
【訂正対象書類名】明細書
【訂正対象項目名】００９０
【訂正方法】変更
【訂正の内容】
【００９０】
図４で述べたように、タイミングは、時間を持つ検査ファンクションを正確に反応させるか、タイムリーな一時的な遷移を検査するかのいずれかの、検査のオートマトンの遷移上に仕様が記載されている。タイミングは、特定された範囲において変化することができ、それから検査は、各遷移のために特定された範囲の元で、ハザード呼び出し時間の生成と合わせられ得る。検査の遷移上にトリガーを追加することも可能である。そのようなトリガーは、ユーザ要求の完了またはシステム応答制限に対応する。例えば、もしユーザ要求が「１００km/hのスピードに達する」ことなら、その場合は１００km/hのスピードに達したことを示す信号は、新しいユーザ要求を注意深く読むためのトリガーたり得る。検査のオートマトンにおいては、遷移は、例えば新しいユーザ要求を操作する前でトリガー後に１秒待つ等の、遅延とトリガーの混合になり得る。図５に描かれたシナリオは、例えばユーザ要求がシステムの状態を変化させることができるごとに、これが正当なとき、システムが正確に反応するということだけを検査する。しかしながら、あるユーザ要求が、与えられたコンテキストでの対応するシステム応答を何も持たなかったということが時々要求される。これはある種の「起こらない」ユースケースまたは不可能なユースケースである。
【誤訳訂正１８】
【訂正対象書類名】明細書
【訂正対象項目名】００９１
【訂正方法】変更
【訂正の内容】
【００９１】
検査プランは、不可能なユースケースの検査を含むように、完全なものにすることができ、これらのユースケースは、ある状態において何の答えもないユーザ要求に対応する。これを実行するため、我々は無視されるであろうユーザ要求に対応する補充的な状態と遷移といっしょに、検査シナリオを単に詰める。そのような無視されたユーザ要求は、結果として生じる状態を変化させない。例えばもし遷移５７９が、不可能なユースケースに対応する無視されたユーザ要求を実行するなら、その場合は状態５３７と５３９は、検査中のサービスの同じ状態に対応するだろう。もし動作を簡単にするなら、もしいくつかの遷移が取り消されるなら、生成された検査シナリオはいまだ正当だが、部分的だろう。
【誤訳訂正１９】
【訂正対象書類名】明細書
【訂正対象項目名】０１１２
【訂正方法】変更
【訂正の内容】
【０１１２】
図１１では、サービスと実証の種々のステップの設計プロセスが描かれている。設計の進歩の段階の間、特徴の最初のモデルの作成まで実証は不可能である。そこで、ユースケースの仕様１１０１、動作に関するオートマトンからなる動作に関する仕様１００３、その動作に関するオートマトンの各状態の中でどのファンクションが動作しているのかを示す機能的な仕様１１０５が一旦作られると、それからサービスのモデルを得るために各ファンクションのモデルを作ることが可能である。一旦、このモデルが得られると、その入力と出力は、「原理上は」センサ、アクチュエータおよび他のサービスとのやり取りである。
【誤訳訂正２０】
【訂正対象書類名】明細書
【訂正対象項目名】０１１３
【訂正方法】変更
【訂正の内容】
【０１１３】
このステップで、検査プランを自動的に生成することが可能であり、検査モデルは図４と５に描かれた。その場合、環境ループは、入力と出力としてそのモデルの入力と出力を取ることができる。これは例えば命令とデータ収集のドライバの統合を排除する。車両のドア施錠サービスの場合、あり得る入力は、ユーザからの施錠要求のフォーマットされたメッセージであってもよく、あり得る出力は、車両のドアを施錠するリレーの命令であってもよい。ブロック４１７に挿入されたモデルは、図２に表されたような形であってもよい。ユースケースのレベルと機能的なレベルでタイミング要求を推定するのが既に可能であるが、このステップでのタイミングは大ざっぱに推定される。しかしながら、このステップでのタイミングは物理的なアーキテクチャーから実証されないだろう。
【誤訳訂正２１】
【訂正対象書類名】明細書
【訂正対象項目名】０１２２
【訂正方法】変更
【訂正の内容】
【０１２２】
図１２では、我々は、安全システムのための特定の開発プロセスに焦点をあてる。そのプロセスは次のステップからなり、ユースケースのリスト（図１１の１１０１）と動作仕様（図１１の１１０３）の形式のもとで、一旦、動作説明１２０１がなされる
１ 望ましくないイベントとそれらの重要性の同定（１２０３）
２ その現実のまたは仮想のセンサとアクチュエータで形成されたシステムの機能的仕様（１２０５）
３ リンプホーム（Limp-home） モードの記述（１２０７）
４ 望ましくないイベントの現実のまたは仮想のアクチュエータへの関連付け（１２０９）
５ 機能的アーキテクチャー上の望ましくないイベントの精錬（refinement）（１２１１）
６ 安全要求精錬を伴った冗長度の導入（１２１３）
７ ハードウェア アーキテクチャーの定義（１２１５）
８ 電子的制御ユニット上のファンクションのマッピング（１２１７）
９ 得られた電子的アーキテクチャーのフォールトトレランスの実証（１２１９）
１０ 物理的コンポーネントと配線の幾何学的マッピング（１２２１）
１１  得られた電気-電子的アーキテクチャーのフォールトトレランスの実証（１２２３）
このプロセスは線形であるように意図されない。少しのループは、説明において隠される。例えばステップ６は、多数のやり直しを生じるかもしれない種々の方法によって実装することができる。また、種々のハードウェアアーキテクチャーは、目標が、与えられたフォールトトレラント要求の元でよりコストのかからないアーキテクチャーを見つけるように、ステップ７において調査することができる。ステップ８では、特にもしステップ９が、１つのマッピングが満足でなく、もっと作業することが明らかになったならば、種々のマッピングが調査される。また、ステップ１０では、ノードの種々の位置を調査することができる。
【誤訳訂正２２】
【訂正対象書類名】明細書
【訂正対象項目名】０１５８
【訂正方法】変更
【訂正の内容】
【０１５８】
共通のユースケースを共有するサービスの１つのセットを我々が検査する場合、同期が、これらのサービスの検査オートマトンの間で遂行されなければならない。検査中のすべてのサービスのために共通のユースケースが同期して実行される制限と共に、検査は織り混ぜられなければならない。これは遂行するのが難しくない。しかしながら、この検査アプローチは、横断的影響を有するユースケースが準備段階で正しく同定された条件の元で妥当である。
【誤訳訂正２３】
【訂正対象書類名】明細書
【訂正対象項目名】０１６８
【訂正方法】変更
【訂正の内容】
【０１６８】
用語解説：（導入された順番にほぼ従っている）
ユースケース（Use Case）：１つのサービスの使用の要素的なシナリオの記述。１つのユースケースは、コンテキストの定義、ユーザ要求、システム応答からなり、また例えばエンドツーエンドの実行時間のようなパフォーマンス要求も含んでもよい。
【誤訳訂正２４】
【訂正対象書類名】明細書
【訂正対象項目名】０１７０
【訂正方法】変更
【訂正の内容】
【０１７０】
ユースケースコンテキスト（Use Case Context）：ユースケースが利用できる、例えば機械的および電気的コンポーネントの状態等のコンテキスト。
【誤訳訂正２５】
【訂正対象書類名】明細書
【訂正対象項目名】０１７４
【訂正方法】変更
【訂正の内容】
【０１７４】
スケルトン実証環境（Skeleton validation environment）：検査または実証環境のための、基本的な輪郭およびデータフローを含む、検査環境のモデルのテンプレート。
【誤訳訂正２６】
【訂正対象書類名】明細書
【訂正対象項目名】０１８４
【訂正方法】変更
【訂正の内容】
【０１８４】
スケルトン実証環境（Skeleton validation environment）：すべてのファンクションが、検査中のサービス以外の部分では、恒等ファンクションである、実証環境の特定の実施例。スケルトンの目的は、関連する検査オートマトンと共に実証環境の複合的なデータフローを生成することである。スケルトンが一旦自動的に生成されると、それはモデル  イン  ザ  ループのフェーズで完成され、実証され得る。
【誤訳訂正２７】
【訂正対象書類名】図面
【訂正対象項目名】図１１
【訂正方法】変更
【訂正の内容】
【図１１】
2007528069.tif 000001