この例では,設計エラー検出解析を使用して,モデル内の整数オーバーフローエラーを検出する方法を示します。万博1manbetx仿真软件®设计校验™は,結果として整数オーバーフローに至る可能性のあるモデル構造を特定し,シミュレーション中に整数オーバーフローが発生することがないと証明するか,または,整数オーバーフローエラーを示すテストケースを生成するかのいずれかを行います。

この例では,万博1manbetx仿真软件®设计校验™のプロパティ証明解析を使用した,プロパティ違反の検出方法を示します。安全要件をプロパティとしてモデル化してから，要件に対して設計モデルを検証します。

この例では，すべてのモデルカバレッジを達成するテストケ，スの生成方法を示します。既定の設定では,万博1manbetx仿真软件设计校验は最小ステップでオブジェクティブを達成するテストケースを生成します。いずれか1つのテストオブジェクティブにより,πコントローラーの離散積分器がその上限を超過するように強制されます。制約なしで仿万博1manbetx真软件设计校验を実行する場合,速度を500に強制することにより,この制限は単一のステップで超過します。速度の制約により，テストケ，スの値は0 ~ 100の間で制限されます。これにより、テストケ、スはいく、かのサンプルをとり、積分器の制限を超えるように強制されます。