检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

使用扩展区间时序逻辑为并发工作流建模

西安电子科技大学学报 2007年第4期34卷 673-680页

作者：雷丽晖段振华西安电子科技大学计算理论与技术研究所陕西西安710071

针对集中式体系结构并发工作流的两种运行方式(活动并发执行和活动以任意顺序执行),对区间时序逻辑进行扩展,提出两个新操作符"交错"和"限制性交错".根据工作流状态的偏序关系以及逻辑公式连接前后其模型的长度关系,证明用新操作符连接... 详细信息

针对集中式体系结构并发工作流的两种运行方式(活动并发执行和活动以任意顺序执行),对区间时序逻辑进行扩展,提出两个新操作符"交错"和"限制性交错".根据工作流状态的偏序关系以及逻辑公式连接前后其模型的长度关系,证明用新操作符连接的区间时序逻辑公式适于表示并发工作流.结合一个并发工作流实例,说明如何用扩展区间时序逻辑表示活动及由活动组建的并发工作流,从而得到并发工作流的区间时序逻辑模型.利用并发工作流的区间时序逻辑模型验证并发工作流的活性和安全性,可大大提高并发工作流设计的可靠性.

关键词：并发工作流区间时序逻辑确定有限自动机

在线全文

学校读者我要写书评

暂无评论

基于有穷论域下区间时序逻辑的模型检测研究

计算机与数字工程 2018年第7期46卷 1302-1305,1451页

作者：李超西安邮电大学计算机学院

通过结合自动机技术实现了有穷论域区间时序逻辑的判定算法,给出了有穷论域下区间时序逻辑变量、函数的处理方法,并提出了利用自动机进行系统建模的方法。最终实现了一个基于有穷论域区间时序逻辑的模型检测工具。

关键词：区间时序逻辑模型检测自动机

具有程序的静态结构和动态行为语义的时序逻辑

在线全文

学校读者我要写书评

暂无评论

计算机研究与发展 2016年第9期53卷 2067-2084页

作者：陈冬火刘全金海东朱斐王辉苏州大学计算机科学与技术学院江苏苏州215006 符号计算与知识工程教育部重点实验室(吉林大学) 长春130012

提出一种区间分支时序逻辑——控制流区间时序逻辑(control flow interval temporal logic,CFITL),用于规约程序的时序属性.不同于计算树逻辑(computation tree logic,CTL)和线性时序逻辑(linear temporal logic,LTL)等传统的时序逻辑,CFITL公式的语义模型不是基于状态的类Kripke结构,而是以程序的抽象模型控制流图(control flow graph,CFG)为基础所构建的含序CFG结构.含序CFG是CFG的一种受限子集,它们的拓扑结构可映射为偏序集,这样诱导产生的自然数区间可自然地用于描述定义良好的程序结构.这种结构含有程序的静态结构信息和动态行为信息,换而言之,CFITL具有规约程序实现结构属性和程序执行动态行为属性的能力.在定义CFITL的语法和语义的基础上,详细讨论了CFITL的模型检验问题,包括基于值状态空间可达性计算的模型检验方法和基于SMT(satisfiability modulo theories)的CFITL有界模型检验方法.现代程序都含有复杂且具有无限值域的抽象数据类型及各种复杂的操作,CFITL语义定义相比CTL等时序逻辑更复杂,因此,基于显示状态搜索的方法难以有效进行,而基于SMT的CFITL有界模型检验方法更易实现、更具有可行性.最近开发相关的原型工具,并进行相关的实例研究.

关键词：区间时序逻辑控制流程图程序静态结构模型检验可满足性模理论

在线全文

学校读者我要写书评

暂无评论

扩展Tempura语言统一模型检测算法

华南理工大学学报（自然科学版） 2011年第7期39卷 163-168页

作者：朱维军周清雷张海宾郑州大学信息工程学院河南郑州450001 西安电子科技大学计算机学院陕西西安710071

针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间... 详细信息

针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序逻辑公式所描述的性质.具体方法是首先翻译规范程序到命题扩展区间时序逻辑公式,然后使用该逻辑的公式满足性判定算法进行自动验证.验证实例证实了新方法的有效性.

关键词：模型检测扩展Tempura语言区间时序逻辑区间模型程序规范统一框架

在线全文

学校读者我要写书评

暂无评论

多速率混合系统的模型检查

西安电子科技大学学报 2008年第1期35卷 60-64,86页

作者：张海宾段振华西安电子科技大学计算机学院陕西西安710071

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质.首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式.接着定义了初始化的多速率自动机状态空... 详细信息

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质.首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式.接着定义了初始化的多速率自动机状态空间上的等价关系及其对应的域自动机,并且通过构造域自动机对应的标注有限状态自动机,把初始化的多速率混合系统的模型检查问题等价地转换成了可解的区间时序逻辑的模型检查问题.利用区间时序逻辑的模型检查算法加上上述的转换规则,就可以解决初始化的多速率混合系统的模型检查问题.

关键词：模型检查混合系统多速率自动机区间时序逻辑

在线全文

学校读者我要写书评

暂无评论

高阶时段演算及其完备性

中国科学（E辑） 2001年第1期31卷 71-85页

作者：詹乃军中国科学院软件研究所开放实验室北京100080

研究如何用时段演算来刻画程序的实时行为 .在实时程序设计里 ,程序变量被解释成时间的函数 .为了定义局部变量声明的语义 ,必须引进关于程序变量的量词 .因此 ,建立高阶时段演算是必要的 .首先建立了高阶时段演算理论 ,然后 ,用高阶时... 详细信息

研究如何用时段演算来刻画程序的实时行为 .在实时程序设计里 ,程序变量被解释成时间的函数 .为了定义局部变量声明的语义 ,必须引进关于程序变量的量词 .因此 ,建立高阶时段演算是必要的 .首先建立了高阶时段演算理论 ,然后 ,用高阶时段演算去验证了一些程序的实时性质 ;最后 ,在假设所有程序变量均有穷可变的条件下 ,证明了高阶时段演算在抽象时间域上是完备的 .

关键词：高阶时段演算超稠密计算完备性程序变量程序设计区间时序逻辑

在线全文

学校读者我要写书评

暂无评论

混合投影时序逻辑与混合系统的形式化验证

计算机科学 2007年第11期34卷 279-282页

作者：张海宾段振华西安电子科技大学计算机学院西安710071

为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑(Hybrid Projection Tempora... 详细信息

为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑(Hybrid Projection Temporal Logic,简称HPTL),既能刻画混合系统的性质,又能表示混合系统的实现。这样,混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时,给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。

关键词：混合系统混合自动机区间时序逻辑形式化验证

在线全文

学校读者我要写书评

暂无评论

基于PVS的ITL定理证明方法

郑州大学学报（理学版） 2009年第4期41卷 31-34,44页

作者：朱维军王迤冉周清雷郑州大学信息工程学院郑州450001 周口师范学院计算机科学系河南周口466001

介绍了区间时序逻辑ITL的语法、语义和公理系统以及通用的辅助定理证明工具PVS,研究了嵌入ITL到PVS的原理,给出了描述ITL的PVS模块,并给出一个实例,实现了基于PVS的ITL推理.在此基础上可以进一步实现基于PVS的多种扩展ITL推理.

关键词：区间时序逻辑原型验证系统辅助定理证明

在线全文

学校读者我要写书评

暂无评论

简讯

西安电子科技大学学报 2011年第1期38卷 53-53页

英国德蒙特福德大学计算机科学技术学院软件技术实验室高级研究员***教授日前来校讲学访问．来访期间，***教授分别作了题为“用时间倒序转换时序逻辑”、“使用itl和tempura进行组合推理”、“无穷模型下的命题区间时序逻辑的完全公理... 详细信息

英国德蒙特福德大学计算机科学技术学院软件技术实验室高级研究员***教授日前来校讲学访问．来访期间，***教授分别作了题为“用时间倒序转换时序逻辑”、“使用itl和tempura进行组合推理”、“无穷模型下的命题区间时序逻辑的完全公理系统”、“使用时序逻辑分析时序逻辑，基于时序逻辑的分层方法”的专题讲座，并与学校师生就相关问题进行了深入交流．

关键词：区间时序逻辑计算机科学技术软件技术组合推理公理系统逻辑分析专题讲座分层方法