Deadlock-freeness

Systems and Software Verification
9. Deadlock-freeness
システム情報科学府情報工学専攻
荒木研究室修士2年住田辰雄
目次
•
•
•
•
9.0 デッドロック
9.1 安全性，それとも活性？
9.2 与えられたオートマトンのデッドロック
9.3 抽象化に注意せよ！
2006/10/4
モデル検査勉強会
2
9.0 デッドロック
• デッドロックが存在しない
– システムはそれ以上進行できないような状態
に到達することは決してない
2006/10/4
モデル検査勉強会
3
9.1 安全性，それとも活性？
•
デッドロックが存在しない
–
–
AG EX true
理論的には安全性ではない
• AG -形式の論理式に変換することはできない
1. モデル検査ツールがAG EX trueを扱うことが可能な
らば，デッドロックは検証できる
2. 安全性に束縛される方法をあてにすることでは，
デッドロックを検証することは不可能である（第11
章）
3. モデル検査ツールがAG EX trueを扱うことが不可
能ならば，検査しようとしているオートマトンに限定し
たデッドロックを直接記述することができる
2006/10/4
モデル検査勉強会
4
9.2 与えられたオートマトンのデッドロック
• オートマトンAはデッドロックが存在しない
– s1 : xとyの値が常に等しい
– s2 : xとyの値が常に異なる
– s3 : 決して到達しない
2006/10/4
モデル検査勉強会
5
9.2 与えられたオートマトンのデッドロック
• デッドロック状態
– s3においてxの値が0以下である
– A |= AG(s3  x  0) (9.1)
• これは安全性である
– AG -形式の論理式である
2006/10/4
モデル検査勉強会
6
9.2 与えられたオートマトンのデッドロック
• オートマトンA’
– s2からs1への遷移を禁止する
– Aにおいて満足される全ての安全性を満たす
• しかしA’にはデッドロックが存在する
– (9.1)はもはやデッドロックを表現していない
2006/10/4
モデル検査勉強会
7
9.3 抽象化に注意せよ！
• A’からA’’へ行われる抽象化操作は安全性
と両立する
• A’’にデッドロックが存在しなくても，A’がそ
うであると証明することにはならない
2006/10/4
モデル検査勉強会
8

Download Report