南京大学：模型检测（PPT课件讲稿）Model Checking

模型检验的过程 建模( Modeling) 规约( Specification) ■验证( Verification)

模型检验的过程 ◼ 建模（Modeling） ◼ 规约（Specification） ◼ 验证（Verification）

模型检验 在模型检验中涉及两种形式说明语言: 性质说明语言用于描述系统的性质 模型描述语言用于描述系统的模型。 模型检验技术用于检验由模型描述语言描述的系 统模型是否满足由性质说明语言描述的系统性质

模型检验 ◼ 在模型检验中涉及两种形式说明语言： 性质说明语言用于描述系统的性质; 模型描述语言用于描述系统的模型。 ◼ 模型检验技术用于检验由模型描述语言描述的系 统模型是否满足由性质说明语言描述的系统性质

模型检验 OK Finite-state mode or Model Checker Error trace (→◇9) Line 5 Line 15 Temporal logic formula Line 21. Lin Line 27

模型检验 Finite-state model Temporal logic formula Model Checker (F W) OK Error trace or Line 5: … Line 12: … Line 15:… Line 21:… Line 25:… Line 27:… … Line 41:… Line 47:…

Model Checking System Train Control System e y=l =16y=10 Specification No collision Modeling e3y=5 Whether State"Collision"Can Be reached in System behavior? Not reachable Input: Enumerate all the Check HA Model DANGEROUSReachable potential behaviors which Return the Specification can reach the target path

Modeling System： Train Control System Specification： No Collision！ Whether State “Collision” Can Be Reached In System Behavior? Input: HA Model Specification Enumerate all the potential behaviors which can reach the target Check Not reachable Reachable Return the path Model Checking

Kripke Model Kripke Structure Labeling Function o Let ap be a non-empty set of atomic propositions o Kripke Model: M=(S, So,R, L) finite set of states 0 S initial state RcS×S transition relation L:S→2AP labeling function

Kripke Model ◼ Kripke Structure + Labeling Function  Let AP be a non-empty set of atomic propositions.  Kripke Model: M = (S, s0 , R, L) S finite set of states s0S initial state RS  S transition relation L: S→2AP labeling function