论文部分内容阅读
模型检验技术是开发高可信系统的重要途径。提出了一种基于定理证明的模型验证方法，并实现了工具验证。它以代数规约语言CafeOBJ描述系统的无限状态并把它转换成有限状态的SMV规约。通过观察迁移系统，证明产生的SMV规约的反例即CafeOBJ规约的反例，来找出开发早期阶段的系统的潜在错误，从而避免时间、金钱的耗费及重复性的劳动。