检索结果-内蒙古大学图书馆

计算机科学 2020年第9期47卷 204-212页

作者：骆翔宇许杭娜曾昊晟陈祖希杨帆华侨大学计算机科学与技术学院福建厦门361021 华侨大学机电及自动化学院福建厦门361021

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实... 详细信息

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。

关键词：符号化模型检测时态测试器实时线性动态逻辑离散实时系统

来源：评论

学校读者我要写书评

暂无评论

实时分支时态逻辑RTCTL*符号化模型检测与树状反例生成

实时分支时态逻辑RTCTL*符号化模型检测与树状反例生成

引用

作者：黄欣玥华侨大学

学位级别：硕士

随着计算机与软件系统越来越广泛地应用于安全关键领域,为了避免潜在的严重后果,软件安全问题愈发受到重视。模型检测技术是一种有效的形式化验证方法,能够验证系统的正确性,并给出能够指示错误的信息。经典的基于自动机的模型检测中,... 详细信息

随着计算机与软件系统越来越广泛地应用于安全关键领域,为了避免潜在的严重后果,软件安全问题愈发受到重视。模型检测技术是一种有效的形式化验证方法,能够验证系统的正确性,并给出能够指示错误的信息。经典的基于自动机的模型检测中,自动机组合的困难限制了对于规约的高效构造。时态测试器是一种特殊的非确定性自动机,通过增加布尔输出变量,能够从自底向上地构造时态逻辑对应的时态测试器,运用时态测试器可以实现高效的模型检测。反例是模型检测的重要特性,但目前对于反例的研究并不足够,大部分模型检测工具生成的反例较为简单,对于带有分支的时态逻辑并不完备,且不能够方便用户理解。本文的主要工作如下: (1)提出一种RTCTL*正时态测试器的构造方法,及其对应的符号化模型检测算法,显著地提升了RTCTL*模型检测的性能。本文证明了提出的RTCTL*正时态测试器构造的完备性,并证明了模型检测算法时间复杂度与所验证模型大小线性相关,与待验证规约长度指数相关。 (2)拓展了CTL*的树状反例结构并提出了对应的反例图。本文拓展了树状反例的结构,通过为反例的节点与边附上必要的注释信息,使反例对于用户更加易于理解。 (3)提出一种基于测试器的模型检测算法为ACTL*生成完备且信息丰富的树状反例的方法。此外,反例图中的所有分支都是具有最短前缀的拉索路径。本文还采取了一些优化策略用以减少注释的数量,并尽量避免构建套索路径。 (4)开发了一个基于有序二元决策图(OBDD)的模型检测工具MCTK2,在其中实现了以上的模型检测与反例图生成算法,并与模型检测工具nu Xmv和MCMAS分别在验证性能与反例阐释效果上进行了实验比较,证明了MCTK2的优越性。

关键词：符号化模型检测时态测试器 RTCTL* 树状反例 MCTK2

来源：评论

学校读者我要写书评

暂无评论

模型检测离散实时线性动态逻辑

模型检测离散实时线性动态逻辑

引用

作者：许杭娜华侨大学

学位级别：硕士

实时系统被广泛地应用在一些重大、紧急的事件的处理中,例如智能机器人、航天系统和铁路调度系统等。实时系统一旦发生错误,后果往往是十分危险甚至可能是灾难性的,这要求实时系统必须具备较高的正确性保证系统中各模块具体的响应时间... 详细信息

实时系统被广泛地应用在一些重大、紧急的事件的处理中,例如智能机器人、航天系统和铁路调度系统等。实时系统一旦发生错误,后果往往是十分危险甚至可能是灾难性的,这要求实时系统必须具备较高的正确性保证系统中各模块具体的响应时间。模型检测技术对于实时系统的可靠性的检测有很好的帮助。但目前已有的模型检测时态部分的实时拓展主要是基于传统时态逻辑之上进行拓展的,缺乏正则属性的表达能力,无法描述复杂实时系统的一些行为。为此,本文在线性动态逻辑(Linear Dynamic Logic,LDL)的基础之上添加时间区间约束,提出一种具有表达离散实时性质和所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL),因此它能够很容易地描述一些复杂实时系统的行为。然后基于构造测试器的方法提出离散实时线性动态逻辑的符号化模型检测算法,接着将所构造的测试器翻译成具体的smv程序模块,在著名模型检测工具nuXmv上运行该测试器的smv模块,实现所提出的算法。本文的主要工作如下:(1)提出离散实时线性动态逻辑RTLDL,它是LDL实时性的扩展,使得LDL能够表达和分析系统的实时行为;(2)借鉴程序控制流标记的思想为基本的时态算子构造时态测试器,解决LDL的模型检测问题。在此基础上进一步构造有界时态公式的测试器,提出了一种基于测试器的RTLDL符号化模型检测算法;(3)在模型检测器nuXmv上使用翻译方法实现并验证我们的算法。实验结果表明,在验证RTLDL公式时,我们的方法在变量、状态空间以及时间方面均明显优于目前唯一实现LDL模型检测的模型检测工具MCMAS-LDLK,特别是对于不包含有界的测试公式嵌套在柯林星中的RTLDL公式验证,我们的算法效果指数级地优于MCMAS-LDLK。

关键词：符号化模型检测时态测试器线性动态逻辑离散实时系统

来源：评论

学校读者我要写书评

暂无评论

基于反例引导抽象精化的有限实时线性时态逻辑模型检测

基于反例引导抽象精化的有限实时线性时态逻辑模型检测

引用

作者：陈木水华侨大学

学位级别：硕士

在绝大多数模型检测中,安全性作为一类重要的属性,常用于验证系统是否满足期望属性的定性分析,即验证系统满足或者不满足某个安全性,但是不能定量地去分析系统的满足情况。同时,面对状态空间爆炸的问题,大多数基于反例引导抽象精化（Cou... 详细信息

在绝大多数模型检测中,安全性作为一类重要的属性,常用于验证系统是否满足期望属性的定性分析,即验证系统满足或者不满足某个安全性,但是不能定量地去分析系统的满足情况。同时,面对状态空间爆炸的问题,大多数基于反例引导抽象精化（Counter-Example Guided Abstraction Refinement,CEGAR）的模型检测器通常用于验证程序中以断言表示的安全性,无法验证更丰富的时态逻辑。为此,本研究以实时线性时态逻辑（Real-Time Liner Temporal Logic,RTLTL）为基础,提出有限实时线性时态逻辑（Real-Time Liner Temporal Logic over finite traces,RTLTL_f）,在有限路径上解释RTLTL,表示计算机复杂的有限实时交互行为。然后,构造RTLTL_f测试器,基于测试器提出用RTLTL_f表示验证属性的模型检测方法,该方法将准确检测出有限长度的反例,并且引入较少的辅助变量。另外,为避免状态空间爆炸,使得系统验证规模更具有伸缩性,结合了惰性抽象与CEGAR框架,基于可重用与可组合的思想,通过使用时态测试器构造断言抽象可达树,改进抽象精化验证流程,提出基于CEGAR的RTLTL_f模型检测。论文的主要研究工作概括如下:1)针对无限路径系统上模型检测效率问题,提出有限实时线性时态逻辑,该工作在有限语义上解释实时线性时态逻辑,用来刻画实时系统在有限路径上带有时间区间的复杂行为。能够避免模型检测阶段在无限语义上,为了寻找一个可接受的公平路径而付出昂贵的计算代价。2)针对RTLTL_f模型检测问题,提出基于测试器的RTLTL_f符号化模型检测,该工作在有限路径上为RTLTL_f构造了对应实时时态公式的测试器,各个子公式测试器之间进行组合,实现构造任意的RTLTL_f公式测试器。通过将测试器输出断言视为不变式公式,从而将RTLTL_f模型检测问题转变为不变式检测。当不变式被违反,就会产生一条有限反例。通过在Nu Xmv模型检测器上使用翻译的方式构造测试器,成功验证该研究工作的可行性。实验结果表明,在引入较少的辅助变量的情况下,在时间复杂度上呈双指数级小于Nu Xmv-sbmc,所创建的BDD变量数量也呈指数级小于Nu Xmv-sbmc,验证效率明显优于Nu Xmv-sbmc。3)针对RTLTL_f模型检测空间爆炸问题,提出基于CEGAR的RTLTL_f抽象模型检测,该工作结合惰性抽象与CEGAR框架来实现RTLTL_f模型检测,通过重用现有的抽象模型检测工具,提升现有抽象模型检测工具对实时线性时态的验证能力。在Theta模型检测器上同样采用测试器翻译的方式对研究工作进行了实验对比分析。实验结果表明,在较大规模验证系统的情况下,本工作在时间与内存消耗上指数级小于基于测试器的RTLTL_f符号化模型检测方法。

关键词：线性时态逻辑有限路径模型检测抽象精化时态测试器

来源：评论

学校读者我要写书评

暂无评论

基于有限路径的实时线性动态逻辑合成

基于有限路径的实时线性动态逻辑合成

引用

作者：黄澄华侨大学

学位级别：硕士

反应式系统合成是根据给定的规约自动构建正确的反应式系统的问题,主要用于自动生成控制密集型程序。合成的步骤大致是先把规约翻译为自动机,把自动机转化为系统与环境的图博弈,再解博弈得到系统玩家的必胜策略。应用领域有机器人运动... 详细信息

反应式系统合成是根据给定的规约自动构建正确的反应式系统的问题,主要用于自动生成控制密集型程序。合成的步骤大致是先把规约翻译为自动机,把自动机转化为系统与环境的图博弈,再解博弈得到系统玩家的必胜策略。应用领域有机器人运动规划、自动化系统的控制、通信协议的开发等等。本文研究有限路径上的实时线性动态逻辑(Real-time Linear Dynamic Logic on Finite Traces,RTLDLf)的合成。RTLDLf的时态表达力强于有限路径上的线性时序逻辑(Linear Temporal Logic on Finite Traces,LTLf)。虽然与有限路径上的线性动态逻辑(Linear Dynamic Logic on Finite Traces,LDLf)表达力等价,但是其简洁性高于等价的LDLf。现有的LDL合成方法大多基于自动机实现,本文提出的RTLDLf合成方法基于时态测试器实现。时态测试器具有很好的组合性,可方便高效地对复杂LDLf公式进行合成。另外,相比于己有的LDLf自动机翻译是基于Mona的半符号化表示,时态测试器的迁移关系和状态空间都是符号化表示的,基于它的合成可以进一步得益于有序二元决策图的高效符号化算法。本文的主要工作如下: 1)为了提高逻辑的时态表达力和简洁性,首先提出了 RTLDLf逻辑。然后针对RTLDLf自动机的翻译问题,提出了自底向上的RTLDLf时态测试器构造方法:从最底层子公式的测试器开始,根据公式中操作符的类型,一步步组合成整个公式的测试器,时间复杂度O(n)。对于每个长度为n的RTLDLf公式存在大小为O(n)的测试器。 2)针对RTLDLf的合成问题,提出基于时态测试器的RTLDLf合成算法,并且分析了算法的正确性,从测试器的终止条件开始根据迁移关系倒推,然后通过对迁移中环境控制的变量进行全称消去,可以计算出系统的必胜策略。 3)在时态逻辑验证平台JTLV上扩展实现以上内容,形成RTLDLf合成工具,包括公式预处理、时态测试器构造、计算一个系统实现和结果可视化等模块。通过摆渡者难题这一经典规划问题验证了该合成工具的有效性。

关键词：反应式系统合成程序合成有限路径上的线性动态逻辑时态测试器图博弈

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：