期刊文献+
共找到17篇文章
< 1 >
每页显示 20 50 100
集成实时逻辑与Z++语言的形式化方法
1
作者 刘瑞成 张立臣 《计算机工程与设计》 CSCD 北大核心 2005年第11期2887-2890,共4页
Lano提出了一种用形式化方法RTL与Z++结合来建模实时系统的方法,并对RTL进行扩展,增强了RTL的表达能力,但对于时间要求非常严格的系统,有时并不能满足系统实时性的要求。可以进一步结合A.K.Mok方法,对表达系统时间约束的RTL公式进行优化... Lano提出了一种用形式化方法RTL与Z++结合来建模实时系统的方法,并对RTL进行扩展,增强了RTL的表达能力,但对于时间要求非常严格的系统,有时并不能满足系统实时性的要求。可以进一步结合A.K.Mok方法,对表达系统时间约束的RTL公式进行优化,然后再转化为Z++类history中RTL公式,使history中的谓词公式更简要更完整,从而减少了检测时间,提高实时响应能力。 展开更多
关键词 实时逻辑 Z 形式化方法 约束图 时间约束
下载PDF
泰克与躐合作为XILINX FPGA提供实时逻辑调试方案 泰克TLA系列逻辑分析仪和FS2 FPGA View软件为XILINX FPGA提供完整的调试套件
2
《国外电子测量技术》 2006年第11期85-85,共1页
2006年9月20日,泰克公司(NYSE:TEK)与First Silicon Solutions(FS2)公司宣布为泰克TLA系列逻辑分析仪推出FPGAView^TM软件包,对Xilinx FPGA提供实时调试功能。通过使用FPGAView软件,工程师可以对其Xilinx FPGA设计的内部信号实... 2006年9月20日,泰克公司(NYSE:TEK)与First Silicon Solutions(FS2)公司宣布为泰克TLA系列逻辑分析仪推出FPGAView^TM软件包,对Xilinx FPGA提供实时调试功能。通过使用FPGAView软件,工程师可以对其Xilinx FPGA设计的内部信号实施快速简便的测量,并能非常容易地选定某一组内部信号进行测量而不需要重新编译设计。 展开更多
关键词 FPGA设计 VIEW软件 逻辑分析仪 泰克公司 XILINX 实时逻辑 调试方案 TLA
下载PDF
概率实时时态认知逻辑模型检测中抽象技术的研究 被引量:2
3
作者 刘志锋 孙博 周从华 《电子学报》 EI CAS CSCD 北大核心 2013年第7期1343-1351,共9页
概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于P... 概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性. 展开更多
关键词 模型检测 概率实时时态认知逻辑 PTACTLK 状态空间爆炸 抽象
下载PDF
基于时态测试器的实时分支时态逻辑模型检测 被引量:2
4
作者 骆翔宇 黄欣玥 +3 位作者 古天龙 苏开乐 陈祖希 郑黎晓 《软件学报》 EI CSCD 北大核心 2022年第8期2930-2946,共17页
基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL... 基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK2.0.0.完成了MCTK与著名的符号化模型检测工具nu Xmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nu Xmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能. 展开更多
关键词 符号化模型检测 公平离散系统 正时态测试器 实时分支时态逻辑 二元决策图
下载PDF
离散实时线性动态逻辑的符号化模型检测
5
作者 骆翔宇 许杭娜 +2 位作者 曾昊晟 陈祖希 杨帆 《计算机科学》 CSCD 北大核心 2020年第9期204-212,共9页
实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实... 实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。 展开更多
关键词 符号化模型检测 时态测试器 实时线性动态逻辑 离散实时系统
下载PDF
强容错的航空发动机空中停车实时监测逻辑研究
6
作者 赵航 刘金鑫 +1 位作者 詹轲倚 宋志平 《推进技术》 EI CAS CSCD 北大核心 2021年第8期1735-1748,共14页
为了确保航空发动机空中再起动策略或飞行员应急操作的快速执行,设计了一种具备强容错性的空中停车实时监测逻辑。该逻辑组合了风扇转速、压气机转速、涡轮后温度和换算主燃油流量的空中停车故障特征,融合了监测阈值设定、参数变化范围... 为了确保航空发动机空中再起动策略或飞行员应急操作的快速执行,设计了一种具备强容错性的空中停车实时监测逻辑。该逻辑组合了风扇转速、压气机转速、涡轮后温度和换算主燃油流量的空中停车故障特征,融合了监测阈值设定、参数变化范围限制和反向惩罚处理等容错性策略,可适应发动机个体差异及性能衰退、非标准天、传感器正常噪声扰动和单一传感器故障。为检验该逻辑的鲁棒性和容错性,采取按任务剖面运行测试和全包线随机加减速测试相结合的方式。虚警测试和检测性能验证结果表明,当发动机正常运行或发生单一传感器故障时,该监测过程均无虚警;相比于继承自АЛ-31Ф发动机的空中停车监测逻辑,本文提出的监测逻辑具备更好的检测性能;当单一传感器发生故障时,该监测过程的检测性能无降级情况。 展开更多
关键词 航空发动机 空中停车 实时监测逻辑 故障特征 容错性策略
下载PDF
开放式体系结构数控系统实时性的建模与分析 被引量:5
7
作者 曹宇男 张辉 +1 位作者 叶佩青 王田苗 《机械工程学报》 EI CAS CSCD 北大核心 2011年第1期108-116,共9页
给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)... 给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)。TTM/ATRTTL提供一整套方法用于对OAC系统的硬实时性和反馈特性进行建模并使用该形式化方法在系统层对OAC系统进行建模。分别给出开环OAC,系统级逻辑控制器以及任务间通信和同步机制的TTM模型,并最终给出具有调度机制的闭环OAC系统TTM模型。该模型为系统验证体系结构的基础。最后,给出系统验证体系结构并用模型验证工具STeP和CAD工具SF2STeP实现之。在系统验证过程中,首先解决STeP中遇到的若干模型验证问题,这些问题包括重写规则,验证规则,状态爆炸问题,以及时间约束限制问题。通过模型验证试验解决OAC系统运行过程中出现的死锁以及系统各模块执行时间约束检验问题。试验结果表明该方法可以有效地对OAC系统进行建模并对系统的实时特性进行验证。 展开更多
关键词 开放式体系结构数控系统 形式化描述与验证方法 时间转化模型/全时轴实时时态逻辑 实时 建模
下载PDF
基于面向方面的实时系统建模方法 被引量:4
8
作者 刘瑞成 张立臣 《计算机科学》 CSCD 北大核心 2006年第7期262-265,共4页
分布式实时系统的实时特性可以利用面向方面软件设计方法来建模,把时间方面细分为确定的时间子方面、不确定的时间子方面和模糊时间子方面。根据面向方面技术,不同的时间子方面分别利用随机实时时序逻辑(SQTL)和模糊时间Petri网(FTN)来... 分布式实时系统的实时特性可以利用面向方面软件设计方法来建模,把时间方面细分为确定的时间子方面、不确定的时间子方面和模糊时间子方面。根据面向方面技术,不同的时间子方面分别利用随机实时时序逻辑(SQTL)和模糊时间Petri网(FTN)来表示,并且每个不同形式化语言表示的子方面模型能够通过转化为时间自动机织入系统,实现系统的实时特性。 展开更多
关键词 面向方面软件设计 形式化方法 时间自动机 模糊时间PETRI网 随机实时时序逻辑 实时系统
下载PDF
基于时序逻辑的3种网络攻击建模 被引量:5
9
作者 聂凯 周清雷 +1 位作者 朱维军 张朝阳 《计算机科学》 CSCD 北大核心 2018年第2期209-214,共6页
与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式,该方法不能检测出常见的back,ProcessTable以及Saint 3种攻击。因此,使用命题区间时序逻辑(ITL)和实时攻击签... 与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式,该方法不能检测出常见的back,ProcessTable以及Saint 3种攻击。因此,使用命题区间时序逻辑(ITL)和实时攻击签名逻辑(RASL)分别对这3种攻击建立时序逻辑公式。首先,分析这3种攻击的攻击原理;然后,将攻击的关键步骤分解为原子动作,并定义了原子命题;最后,根据原子命题之间的逻辑关系分别建立针对这3种攻击的时序逻辑公式。根据模型检测原理,所建立的时序逻辑公式可以作为模型检测器(即入侵检测器)的一个输入,用自动机为日志库建模,并将其作为模型检测器的另一个输入,模型检测的结果即为入侵检测的结果,从而给出了针对这3种攻击的入侵检测方法。 展开更多
关键词 命题区间时序逻辑 实时攻击签名逻辑 模型检测 入侵检测
下载PDF
构建度量区时序逻辑的时间自动机
10
作者 王勤思 《计算机工程与设计》 CSCD 北大核心 2011年第2期568-571,575,共5页
在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B ... 在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。 展开更多
关键词 模型检测 实时时序逻辑 度量区时序逻辑 基于迁移的扩展时间Buchi自动机 TABLEAU方法
下载PDF
单率异步数据流语言的RTL文法设计
11
作者 王瑞荣 周泓 +1 位作者 耿晨歌 汪乐宇 《工程设计学报》 CSCD 2002年第1期31-35,共5页
数据流语言是面向虚拟仪器的可视化编程环境的核心 .为了使这些基于数据流的编程环境能够应用到实时系统设计中 ,必须引入一种严格定义的实时文法 .RTL文法适合描述数据流语言 ,但是异步节点的表述问题以及时间基准选择问题并未解决 .... 数据流语言是面向虚拟仪器的可视化编程环境的核心 .为了使这些基于数据流的编程环境能够应用到实时系统设计中 ,必须引入一种严格定义的实时文法 .RTL文法适合描述数据流语言 ,但是异步节点的表述问题以及时间基准选择问题并未解决 .提出了一种用于描述单率、异步数据流语言的 RTL文法 .该文法中引入传输事件常量与状态谓词 (state predicates)解决了异步节点的 展开更多
关键词 虚拟仪器 数据流语言 可视化编程 实时系统 实时逻辑 RTL文法 设计
下载PDF
结合形式化方法的UML系统开发 被引量:10
12
作者 罗蜜 张为群 《西南师范大学学报(自然科学版)》 CAS CSCD 北大核心 2003年第2期203-208,共6页
介绍并讨论了在系统开发过程中使用UML(UnifiedModelingLanguage)与其他形式化方法得到的一种精化模型,而且这一模型也同样支持形式化的分析和验证.
关键词 统一建模语言 UML 系统开发 形式化方法 实时动作逻辑 形式化语义 验证规则
下载PDF
施耐德电气发布新型可编程自动化控制器
13
《自动化技术与应用》 2007年第8期135-135,共1页
施耐德电气日前发布了其TE电器品牌的Modicon M340可编程自动化控制器(PAC)产品,除了具有Modicon产品线适用于工业环境的实时逻辑解决平台功能之外,还具有通信、运动、数据库以及处理功能。
关键词 可编程自动化控制器 电气 MODICON TE电器 实时逻辑 工业环境 产品线 数据库
下载PDF
面向方面的时间特性建模
14
作者 高娜 张立臣 刘东星 《计算机工程》 CAS CSCD 北大核心 2010年第13期281-282,285,共3页
基于面向方面软件设计方法,分离出分布式式系统的时间特性作为一个方面单独建模,将时间子方面思想应用到统一建模语言(UML)建模中,利用随机实时时序逻辑和模糊时间Petri网扩展UML约束。实例证明,该建模方法可解决UML语义问题,使建模更准... 基于面向方面软件设计方法,分离出分布式式系统的时间特性作为一个方面单独建模,将时间子方面思想应用到统一建模语言(UML)建模中,利用随机实时时序逻辑和模糊时间Petri网扩展UML约束。实例证明,该建模方法可解决UML语义问题,使建模更准确,且为日后代码织入、自动生成和测试提供方便。 展开更多
关键词 面向方面软件设计 统一建模语言 模糊时间PETRI网 随机实时时序逻辑 实时系统
下载PDF
AN INTELLIGENT METHOD FOR REAL-TIME DETECTION OF DDOS ATTACK BASED ON FUZZY LOGIC 被引量:2
15
作者 Wang Jiangtao Yang Geng 《Journal of Electronics(China)》 2008年第4期511-518,共8页
The paper puts forward a variance-time plots method based on slide-window mechanism tocalculate the Hurst parameter to detect Distribute Denial of Service(DDoS)attack in real time.Basedon fuzzy logic technology that c... The paper puts forward a variance-time plots method based on slide-window mechanism tocalculate the Hurst parameter to detect Distribute Denial of Service(DDoS)attack in real time.Basedon fuzzy logic technology that can adjust itself dynamically under the fuzzy rules,an intelligent DDoSjudgment mechanism is designed.This new method calculates the Hurst parameter quickly and detectsDDoS attack in real time.Through comparing the detecting technologies based on statistics andfeature-packet respectively under different experiments,it is found that the new method can identifythe change of the Hurst parameter resulting from DDoS attack traffic with different intensities,andintelligently judge DDoS attack self-adaptively in real time. 展开更多
关键词 Abnormal traffic Distribute Denial of Service (DDoS) Real-time detection Intelligent control Fuzzy logic
下载PDF
Swinging up a Real-Time Inverted Pendulum System 被引量:1
16
作者 Maher Mohammed AlOmari Saeb Farhan Al Ganideh 《Journal of Mechanics Engineering and Automation》 2011年第5期407-411,共5页
In this study, a real-time control of the cart inverted pendulum system was developed using Mamdani type Fuzzy Logic Controller. Swing-up and stabilization of the inverted pendulum were implemented directly in a Fuzzy... In this study, a real-time control of the cart inverted pendulum system was developed using Mamdani type Fuzzy Logic Controller. Swing-up and stabilization of the inverted pendulum were implemented directly in a Fuzzy Logic Controller. The fuzzy logic controller was designed in the Matlab-Simulink environment and applied into in a Quasar controller board. Swing-up algorithm brings the pendulum near to its inverted position in 5 seconds from downward position. External forces were applied on the inverted pendulum to test the robustness of the fuzzy logic controller under internal as well as external disturbances. The inverted pendulum system showed an acceptable robustness to the external and internal disturbances. 展开更多
关键词 FUZZY CONTROL inverted pendulum.
下载PDF
离散事件系统的面向对象实时时态着色Petri网模型 被引量:2
17
作者 田国会 贾磊 +1 位作者 路飞 姜健 《系统工程理论方法应用》 2001年第3期206-208,共3页
提出了由记时面向对象着色 Petri网为被控对象建模 ,用实时时态逻辑进行系统期望行为规范的实时离散事件系统面向对象实时时态着色
关键词 离散事件系统 PETRI网 实时时态逻辑 面向对象 DEDS RTTL
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部