Model checking (dual-language approacm is a technique for verifying finite state concurrent systems 实际系统 需求 建模 形式化 -Modeling 模型 规范 Convert a design into a formalism 修改 -Automata 模型检测器 Yes No -Specification 反例 结束 State the properties that design must satisfy SPECs are written in propositional temporal logic. Verification Check whether the properties is preserved Verification procedure is an exhaustive search of the state space of the design. If no,a counterexample raises llxx@ustc.edu.cn 10/112Model checking (dual-language approach) • is a technique for verifying finite state concurrent systems – Modeling • Convert a design into a formalism – Automata llxx@ustc.edu.cn 10/112 – Specification • State the properties that design must satisfy – SPECs are written in propositional temporal logic. – Verification • Check whether the properties is preserved – Verification procedure is an exhaustive search of the state space of the design. • If no, a counterexample raises