模型检验(3)(091231) 闵应骅 时态逻辑用来描述正确的系统行为,模型检验提供实用的硬件和软件验证方法。模型验证可形式地描述如下:给定一个有限结构M,状态s,和一个时态逻辑公式,问M, s |= f ?即问:在结构M中,于状态s0,f是否为真?或者说,给定M和f,计算这个集合{s : M, s |= f}。他们证明了 ...
模型检验(1)(091230) 闵应骅 大家承认,计算机领域的ACM图灵奖相当于自然科学的诺贝尔奖。2007年图灵奖授予Edmund M. Clarke,E. Allen Emerson,和Joseph Sifakis。他们创立了模型检验---一种验证技术,用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。如果不能满足,则提供 ...