论文部分内容阅读
当前在计算机科学技术领域，模型检查技术在工业与学术界都受到越来越多的关注与应用，人们已经开发了许多模型检查器来满足各方面研发工作的需求。这些模型检查器采用不同的模型描述语言，运用不同的验证技术，在各领域中发挥着作用。但是对于不是很专业的终端用户而言，选择与当前问题合适的模型检查器并不容易。目前还没有一套标准的系统描述语言能用于各种建模工具以支持模型检查，因此，建立连通不同检查器间的桥梁是一件有意义的工作。 SPIN与NuSMV是目前使用最广泛的两个模型检查器。SPIN被广泛用于构建分布式与并发系统模型，模拟模型中多进程的执行及进程间通信，验证这类复杂模型需要满足的各种性质。SPIN采用按需生成状态空间(on-the-fly)、偏序规约(partialorderreduction)以及压缩技术，能够较好地完成各类性质(特别是LTL描述的性质)的验证工作。而NuSMV支持直接描述状态迁移系统，要求用户通过多个模块的状态迁移描述系统行为。它主要采用二元决策图(binarydecisiondiagram，BDD)与有界模型检查技术(boundedmodelchecking，BMC)来提高验证效率。这两个模型检查器的模型描述语言不同、能够验证的性质类型不同、采用的技术也不同，但是所建立的系统模型是相通的。这是因为如果将进程的变量当前值看成当前状态，那么进程的执行过程实际上也就是一个状态迁移系统进行状态迁移的过程。因此完全有理由相信，基于多进程描述的模型也可以用NuSMV来建模。如果用这两个检查器的不同语言描述同一个模型，就可以采用两套不同技术来验证，而且可验证的性质范围也得到了扩大。 本文工作的主要成果是S2N工具，它能将SPIN的描述语言Promela翻译成NuSMV模型检查器的描述语言。用户只需要输入S2N能处理的Promela描述的模型，S2N便能输出一个与之等价的NuSMV能处理的模型。S2N以语句为基本处理单位对象，SPIN模型里的一条语句对应着状态发生一次迁移。S2N模型转换的实现借鉴了程序计数器的思想。首先在SPIN模型中加入语句标号，用不同的整数值标识不同语句。在作为翻译结果的NuMSV模块里增加一个取值为这些整数值的变量pc，模型运行中的变量随着pc的变化而发生改变，并基于pc模拟SPIN模型里的执行流程。本文将详细介绍这一翻译过程与S2N工具的实现。 通过一批具体的系统模型的试验，可以看到，对于不同的系统和问题，基于SPIN构建的模型与翻译得到的NuSMV模型的运行效率(时间和空间)可能有很大不同。对某些系统模型，通过S2N转换得到的NuSMV模型能较大提高运行效率并降低存储消耗。一般而言，在模型的规模不大，或者需要验证CTL等SPIN无法验证的性质时，S2N提供了一个可行的建模与规范验证方法。