文档介绍：Software Model Checking Software Model Checking for Embedded Systems for Embedded Systems PIs: Matthew Dwyer 1 , John Hatcliff 1 , and e Avrunin 2 Post-docs: Steven Seigel 2 , Radu Iosif 1 Students: Robby 1 , Roby Joehanes 1 , Yu Chen 1 Kansas State University 1 University of Massachusetts 2 The Dream The Dream Program Requirement Checker void add(Object o) { buffer[head] = o; head = (head+1)%size; } Object take() { … tail=(tail+1)%size; return buffer[tail]; } Property 1: … Property 2: …… OK Error trace or Model Checking Model Checking Finite-state model Temporal logic formula Model Checker ??????????????? OK Error trace or Line 5: … Line 12: … Line 15: … Line 21: … Line 25: … Line 27: …… Line 41: … Line 47: … Why use Model Checking? Why use Model Checking? ? In contrast to testing, plete coverage by exhaustively exploring all paths in system, ? It’ s been used for years with good ess in hardware and protocol design ? Automatically check , ., – invariants, safety & liveness properties – absence of dead-lock and live-lock, – complex event sequencing properties, “ Between the key being inserted and the key being removed, the ignition can be activated at most twice. ” This suggests that model-checking can complement existing software quality assurance techniques . What makes model-checking What makes model-checking software difficult? software difficult? ? Model construction OK Error trace or Finite-state model Temporal logic formula Model Checker ?????????????? State explosion Problems using existing checkers: ? Property specification ? Output interpretation Line 5: … Line 12: … Line 15: … Line 21: … Model Construction Problem Model Construction Problem ? Semantic gap: Model Description Model Checker Program void add(Object o) { buffer[head] = o; head = (head+1)%size; } Object take() { … tail=(tail+1)%size; return buffer[tail]; }Gap Programming Languages Model Description Languages methods, inheritance, dynamic creation, exceptio