基于带参系统Murphi模型的SMV自动建模

提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建模比较容易,而且得到的模型代码量比较少,易于阅读、理解和修改;而SMV模型则能实现更丰富的控制,如进行快速不变式检查和限界模型检测等,但是建模过程复杂,模型不易维护.我们通过对两者进行分析,首先提出了能够很好描述带参系统的一个语义模型,然后读入相应的Murphi模型并进行分析以获取其语义模型表示,最后再通过一系列的策略自动得到限定参数时的SMV模型,由此得到的模型能够满足实际科研工作的应用要求.     

Verilog代数语义研究

给出了Verilog的代数语义.这是一个等式公理体系,它将Verilog语义特征通过代数规则简洁而准确地表达出来;并且这个代数语义相对于已经所作的操作语义模型来讲是可靠的,即所有的这些代数规则左右两边的进程在操作语义的观察模型下都是互模拟的.研究了此代数语义的相对完备性,即参照前面的操作语义模型,相对于扩展Verilog语言的一个子集而言,此代数语义是完备的.即所有符合这样语法的程序,如果它们是互模拟等价的,那么它们同样可以在所提出的代数系统中被推导相等.在完备性证明过程中,采用范式方法,即构造一种语法上特殊的程序,任何属于上述子集中的一个程序通过该代数规则都能够被转化为范式程序,而且范式程序在操作语义模型下是互模拟的当且仅当它们是语法相同的.上述结果具有重要的理论意义,因为现有的进程代数理论主要是针对管道通信并行语言而展开的,而对于像Verilog这种以共享变量通信为基础的复杂并行语言研究还是比较少的,对此类复杂的基于共享变量的并行语言的进程代数理论研究提出了一种通用、有效的方法.     

基于不变量查找的German协议验证

提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.     

Verilog语言形式化语义研究

在连续离散混合时间模型中考虑Verilog的语义行为,将混合模型中的一个区间作为Verilog程序一次运行过程的指称.提出了一种扩展的ITL来描述这种混合区间,从而给出Verilog的形式语义.这种语义定义不仅考虑到了各种语言成分的最终执行结果,而且能够很好地给出语言成分执行的时序特征.