时间符号迁移图及其互模拟判定

引入时间符号迁移图的概念 ,作为既涉及通讯又具有实时性的并发系统的模型 .该文给出了这种迁移图时间互模拟的算法 。

基于符号迁移图的互模拟验证算法

符号迁移图是传值进程的一种直观而简洁的语义表示模型。该模型由Hennessy和Lin首先提出 ,随后又被Lin推广至带赋值的符号迁移图。本文不但定义了符号迁移图各种版本 (基 /符号 )的强操作语义和强互模拟 ,提出了相应的强互模拟算法 ,而且通过引入符号观察图和符号同余图 ,给出了其弱互模拟等价和观察同余的验证算法 ,给出并证明了τ 循环和τ 边消去定理 ,在应用任何弱互模拟和观察同余验证算法之前 ,均可利用这些定理对所给符号迁移图进行化简。

时间符号迁移图上的可达性分析

提出了以时间符号迁移图为建模语言、基于可达性分析的模型检测算法 ,并给出了算法的正确性证明 .

带赋值符号迁移图的局部优化算法

带赋值符号迁移图（ＳＴＧＡ）是刻画一般传值进程的抽象计算模型，在ＳＴＧＡ 上可以用“ｏｎ－ｔｈｅ－ｆｌｙ”实例化算法来验证传值进程之间的互模拟等价．由于ＳＴＧＡ 的一个结点对应于具体迁移图的许多结点，在ＳＴＧＡ 上所作的优化对提高互模拟判定算法的时间和空间效率会产生很大的影响．文中介绍了ＳＴＧＡ 上的一组局部优化算法，证明其正确性，并通过应用实例说明对提高效率的作用．

π-演算的符号迁移图及其早互模拟验证算法

提出符号迁移图作为π 演算进程直观而高效的表示模型 ,并给出了符号迁移图多种版本 (强 /弱 ,基 /符号 )的早操作语义 ,在此基础上定义了相应版本的早互模拟和观察同余 .同时引入了符号观察图和符号同余图以及τ 循环和τ 边消去定理 .最后给出了关于强 /弱早互模拟等价和早观察同余的符号验证算法 ,并证明了其正确性 .将关于传值进程的强互模拟验证算法和关于纯CCS的弱互模拟和观察同余的验证技术融合和推广至有穷控制π 演算 .

非对称_(χ-)演算的符号互模拟验证算法

非对称χ-演算是一种移动计算模型。文介绍非对称χ-演算的语法和符号操作语义,给出非对称χ-演算的符号互模拟的验证算法,该算法根据算法输出的谓词等式系,求解最大符号解。并证明算法正确性,这在一定程度上为今后的自动机验证提供了理论基础。

STGA的变种及其互模拟验证

为刻画和验证无穷值域上的传值进程，Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型，并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题，该文首先引入了ＳＴＧＡ的一个变种，它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒，因而可定义此种ＳＴＧＡ结点间的符号双迁移关系．文中提出了从正则传值进程生成此类ＳＴＧＡ的全部产生规则，并基于Ｌｉｎ的迟强互模拟算法给出了针对此类ＳＴＧＡ的早强互模拟算法．然后利用符号双迁移关系引入了带赋值的早符号观察图（ＥＳＯＧＡ）和早符号同余图（ＥＳＣＧＡ），将上述算法推广至早弱互模拟等价和早观察同余的情况．但符号迁移上赋值的出现有可能导致ＥＳＯＧＡ和ＥＳＣＧＡ为无穷图，从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限．最后，作为一种可应用的情况，进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题．此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图，因而我们的弱互模拟等价算法是可行的．与此同时，文中还给出并证明了符号迁移图上的τ－循环和τ－边消去?

嵌套谓词等式系与弱互模拟

带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解．

一种基于时间自动机的实时系统测试方法

基于时间自动机(timedautomata,简称TA)的一种变体——时间安全输入/输出自动机(timedsafetyinput/outputautomata,简称TSIOA),提出了一种实时系统测试方法.该方法首先将时间安全输入/输出自动机描述的系统模型转换为不含抽象时间延迟迁移的稳定符号状态迁移图(untimedstabletransitiongraphofsymbolicstate,简称USTGSS);然后采用基于标号迁移系统(labeledtransitionsystem,简称LTS)的测试方法来静态生成满足各种结构覆盖标准的包含时间延迟变量迁移动作序列;最后,给出了一个根据迁移动作序列构造和执行测试用例的过程,该过程引入了时间延迟变量目标函数,并采用线性约束求解方法动态求解迁移动作序列中的时间延迟变量.

带复杂数据结构的模型检测工具

模型检测是近二十几年来最成功的自动验证技术之一 ,而模型检测工具的开发是将模型检测和实际相结合的关键 为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测 ,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作 ,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图

面向传值进程的一阶模态逻辑的可判定性与模型检测

对于面向传值进程的Hennessy—Milner逻辑的一阶扩充HML(FO),给出了基于带赋值的符号迁移图的语义解释.证明了HML(FO)的子逻辑HML(FO2)是满足性可判定的,并且讨论了判定的复杂性.最后给出传值进程关于HML(FO2)的模型检测的可判定性结果.

面向实时传值系统的局部模型检测

为对实时传值系统进行模型检测，本文给出了时间符号迁移图作为系统的建模语言，以及实时谓词μ演算作为刻画性质的逻辑语言。本文给出了基于时间符号迁移图和实时谓词μ演算的一个模型检测算法，该算法动态生成和检测可达的状态空间，并且采用对数据变量on—the—fly实例化以及动态切分时间计值集合的方法，是一个局部算法。该算法不仅能处理基于有限域的变量，还可处理一类数据域无穷的变量(称“数据无关”变量)。