Safety Properties

Systems and Software Verification
7. Safety Properties
システム情報科学府情報工学専攻
荒木研究室修士2年住田辰雄
目次
•
•
•
•
•
7.0 安全性
7.1 時相論理における安全性
7.2 形式定義
7.3 実際の安全性
7.4 履歴変数法
2006/9/28
モデル検査勉強会
2
7.0 安全性
• 安全性
– 特定の条件において，望まれないイベントは
決して起こらない
• 2つのプロセスが同時にcritical sectionに入らない
(S1)
• メモリーオーバーフローが起こらない (S2)
• ある状況は不可能である (S3)
• 鍵が点火装置にない限りは，車は始動しない (S4)
– 到達可能性の否定は安全性である
2006/9/28
モデル検査勉強会
3
7.1 時相論理における安全性
• 安全性
– CTL
• 結合子AGを用いて記述する
– AG￢(crit_sec1∧crit_sec2) (S1)
– AG￢overflow (S2)
– PLTL
• 結合子Gを用いて記述する
– G￢(crit_sec1∧crit_sec2) (S1)
– G￢overflow (S2)
2006/9/28
モデル検査勉強会
4
7.1 時相論理における安全性
• 安全性
– 条件が付随する安全性は結合子Wを用いて
記述する
• CTL
– A￢starts W key (S4)
(7.1)
– A￢starts U key
(7.2)
» (7.1)と(7.2)は異なり，(S4)とは一致しない
» (7.2)は安全性ではない
• PLTL
– ￢starts W key (S4)
2006/9/28
モデル検査勉強会
5
7.2 形式定義
• 安全性定義への提案
– 我々がすることが少なければ，安全性が検証
される機会は多くなる
• 全ての安全性を満たす唯一の方法は変わらない
ままで何もしないことである
• もし振る舞いCが性質Pを満たすならば，集約した
振る舞いC’⊆CはPを満たす
2006/9/28
モデル検査勉強会
6
7.2 形式定義
• 構文上の特徴付け


– いかなる安全性もAG 形式で記述すること
ができる
• 
– past時相論理式
» 普通のブール結合子と原子命題と一緒にpast結合
子のみを使用する論理式
• 安全性が違反された場合，すぐにそれに気づくこと
ができるべきである
2006/9/28
モデル検査勉強会
7
7.2 形式定義
• past結合子
– F-1
• Fに対応するpast結合子
• いくつかの過去の瞬間においてφが満たされている
– X-1
• Xに対応するpast結合子
• 前の瞬間においてφが満たされている
– φSψ
• Uに対応するpast結合子
• ψは過去の瞬間において満たされており，それ以来φは満た
されている
2006/9/28
モデル検査勉強会
8
7.2 形式定義
• 例
– AG￢(sc1∧sc2)
– AG(starts => F-1 key)
– ψ1，ψ2 : 安全性の論理式
• ψ1∧ψ2
– 安全性の論理式である
• ψ1∨ψ2
– 安全性の論理式ではない

– (AGP)∨(AGQ)はAG  と等価となる形式が存在しない
2006/9/28
モデル検査勉強会
9
7.2 形式定義
• 反例
– 満たされていない安全性に応じてモデル検査
ツールが提供するメッセージ
-1
– AG F が満たされていないならば，初期状態
から望まれない状態へと続く有限の経路が存
在する
2006/9/28
モデル検査勉強会
10
7.3 実際の安全性
• 現在past時相論理を扱うことのできるモデ
ル検査ツールは存在しない
• past時相論理を組み合わせる利点


– 構文がAG であれば，安全性の論理式であ
ることが保証される
– 過去と未来を組み合わせるような自然な記述
に適しており，豊富な形式化を行うことができ
る
2006/9/28
モデル検査勉強会
11
7.3 実際の安全性


• 形式AG を扱うためのアプローチ
– 過去削除
• past論理式とfuture論理式を組み合わせた時相論
理式は等価な純粋なfuture論理式に変換すること
ができる
AG(  F-1 )  A( W  )
– 履歴変数法
–
2006/9/28
モデル検査勉強会
12
7.4 履歴変数法
2006/9/28
モデル検査勉強会
13
7.4 履歴変数法
-1
• AG(alarm => F crash)
– alarmが鳴るときはいつでも，必ずcrashが事前に起
こっている
• AG(alarm => (￢reset) S crash)
– alarmが鳴るときはいつでも，最後のクラッシュから
resetは起こっていない
• AG(alarm => X -1crash)
– alarmが鳴るときはいつでも，crashが直ちに事前に起
こっている
• h -


–
が真であるかどうか保持するブール変数
2006/9/28
モデル検査勉強会
14
7.4 履歴変数法
h1 : X -1crash
h2 : (reset) S crash
2006/9/28
モデル検査勉強会
15
7.4 履歴変数法
• A+hist
– Aと同じ振る舞いをする
• Aと同じ時相論理式を満たす
– A |= AG (alarm => X -1crash)
• A+hist |= AG (alarm => h1)
2006/9/28
モデル検査勉強会
16

Download Report