組み込みシステムをモデリングするための uppaal と spin/promela の長所と短所は何ですか?
私は少し混乱しています - ありがとう
1 に答える
1
時代遅れの論文ですが、比較に関する有用で関連性のあるポイントがいくつかあります
http://www.brics.dk/RS/96/24/BRICS-RS-96-24.pdf
デザイン
設計言語を考慮すると、明らかな違いは、UPPAAL でリアルタイム システムをモデル化できることです。ケーススタディでは、UPPAAL で興味深い有界ライブネス プロパティを表現および検証できることが示されています。UPPAAL のもう 1 つの有益な機能は、ケース スタディで必要なブロードキャスト動作の非常に自然なモデル化を可能にするコミットされた場所の可能性です。対照的に、PROMELA は送信ステートメントと受信ステートメントのシーケンスに原子性構造を適用できません。
検証
検証フェーズを考えると、UPPAAL のプロパティ言語で表現できるプロパティの種類は、不変プロパティと可能プロパティに制限されます。たとえば、ケース スタディの有界ライブネス プロパティなどのその他のプロパティは、設計を調査する別のテスト オートマトンとして表現する必要があります。セクション 3.4 では、プロパティ言語を拡張し、テスト オートマトンを自動的に生成する方法についてのアイデアを提示します。これは、LTL プロパティを決して自動化しないように変換する SPIN で既に可能です。
于 2015-12-07T18:54:02.543 に答える