SMV的观察迁移系统的模型检测分析

Model checking analysis of observational transition system with SMV

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

Model checking is an important way in developing high confidence systems. A model checking method based on theorem proving is proposed, which describes the infinite system state by CafeOBJ and transfers a CafeOBJ specification to a finite SMV specification, and its tool is implemented. By observing transition system shows that a counter example of a corresponding SMV specification is also a counter example of a CafeOBJ specification. It find errors lurked in systems at earlier stages of their development processes to avoid spending much money and time to correct errors later.