EIT デジタルの無料オンライン教育

定量的モデル検査

説明

さまざまなアプリケーションでのICT(情報通信技術)の統合は、たとえば組み込みおよびサイバー物理システム、通信プロトコル、輸送システムなどで急速に増加しています。 したがって、その信頼性と信頼性はますますソフトウェアに依存しています。 欠陥は致命的で非常にコストがかかる可能性があります(製品の大量生産と安全性が重要なシステムに関して)。

まず、実際のシステムのモデルを構築する必要があります。 最も単純なケースでは、モデルは、システムが到達できるすべての可能な状態と、(ラベル付き)状態遷移システムの状態間のすべての可能な遷移を反映します。 モデルに確率と離散時間を追加するときは、いわゆる離散時間マルコフチェーンを処理します。これは、連続タイミングで連続時間マルコフチェーンに拡張できます。 両方の形式は、多種多様なドメインでのコンピューターと通信システムのモデリングとパフォーマンスおよび信頼性の評価に広く使用されています。 これらの形式はよく理解されており、数学的に魅力的であると同時に、複雑なシステムをモデル化するのに十分な柔軟性があります。

モデルチェックは、モデルの定性的評価に重点を置いています。 正式な検証方法として、モデルチェック分析
システムモデルの機能。 分析が必要なプロパティは、一貫した構文とセマンティクスを持つロジックで指定する必要があります。 次に、モデルのすべての状態について、プロパティが有効かどうかがチェックされます。
このコースの主な焦点は、効率的な計算アルゴリズムについて説明するマルコフチェーンの定量的モデルチェックです。 このコースの学習目標は次のとおりです。

–さまざまな種類の遷移システムの信頼性プロパティを表現します。
–マルコフ連鎖の経時変化を計算します。
–単一の状態が特定の式を満たしているかどうかを確認し、プロパティの満足度セットを計算します。

価格:無料で登録!

言語: 英語

字幕: 英語

定量的モデル検査 –EITデジタル