时段演算

作品数：18被引量：37H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：陈宗基薛乐魏晨韦立安杰更多>>
相关机构：中国科学院软件研究所同济大学北京航空航天大学南京大学更多>>
相关期刊：《电脑知识与技术》《电路与系统学报》《中国安全科学学报》《铁道通信信号》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划广西研究生教育创新计划教育部高等学校骨干教师资助计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于实时自动机的连续时段演算的验证被引量：2
《软件学报》2019年第7期1953-1965,共13页安杰 张苗苗 
国家自然科学基金(61472279)~~
时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑。扩展线性时段不变式是时段演算的重要子集。针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法。该方法将扩展线性时段不变式的有界...
关键词：时段演算 扩展线性时段不变式 量词线性算术 量词消去 
扩展线性时段不变式的模型检验研究进展
《广州大学学报（自然科学版）》2019年第2期10-16,共7页张苗苗 安杰 沈炜 祖佺 
国家自然科学基金资助项目(61472279)
扩展线性时段不变式是时段演算中的一类重要公式.时段演算是周巢尘院士于20世纪90年代提出的一种用于嵌入式实时软件设计的演算系统,它开创性地将积分概念引入计算机实时软件的分析中,从而能够描述处理连续时间区间性质,是国际上公认的...
关键词：时段演算 扩展线性时段不变式 模型检验 实时系统 
连续时段演算的模型检验
《电脑知识与技术》2016年第10期109-111,共3页杨蕊鸿 
扩展的线性时段不变式的模型检验（项目编号：F020106）
模型检验是一种对有限状态系统的性质进行自动检验的技术,能够对系统设计的正确性进行验证.线性时段不变式是一类重要的时段演算公式,它用来描述实时系统的安全性质.而扩展线性时段不变式通过命题逻辑和＆quot;切变＆quot;运算对线性时...
关键词：模型检验 时间自动机 连续时段演算 切变 
概率时段演算的模型检验概述
《电脑知识与技术》2014年第12期8171-8173,共3页吴敏 
在实际工程应用中,越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模,概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时,作为时段演算的一种扩展,概率...
关键词：实时系统 模型检验 概率时间自动机 概率时段演算 
定性/定量集成优化控制器的形式化设计方法
《化工学报》2010年第8期1960-1964,共5页吴锋 
浙江省科技计划重大项目(2008C11017)~~
在化工过程中广泛存在着混杂系统的特性,即系统的信息结构由系统事件和系统状态构成。本文以时段演算为工具提出面向混合信息结构的混杂系统在定性/定量双重指标约束下的形式化设计方法,它将时段演算应用于混杂系统的需求刻划,得出控制...
关键词：混杂系统 时段演算 定性/定量性能 集成优化 
DDS并行模型及其形式化被引量：3
《软件学报》2009年第6期1406-1413,共8页刘真环 韦立 陈艳 赵荣盛 王驹 
国家自然科学基金Nos.60573010;60663001;广西研究生教育创新计划No.2007106020701M52~~
DDS(deadline-driven scheduler)模型是实时系统研究中的一个经典模型,但其原始设置中未提及空间因素.在DDS模型的原始设置上进行扩展,给出了DDS并行模型并在该模型设置下研究带空间限制的任务调度问题.提出了极大空间相容组的概念,并...
关键词：DDS并行模型 全局调度算法 分离逻辑 时段演算 形式化 
高速列车ATP控车模式的形式化模型与安全性分析被引量：1
《中国安全科学学报》2008年第3期28-32,共5页承向军 应志鹏 杜鹏 
轨道交通控制与安全国家重点实验室(北京交通大学)开放课题基金(2008K003)
通过评述当前高速列车的发展现状和趋势,结合我国与欧洲在高速列车应用与相关技术研发方面的差距;对ATP控车模式进行分析,并提出采用时段演算针对实时、连续系统的形式化描述工具;根据时段演算的基本符号、公理、定理和推导规则,建立基...
关键词：高速列车 形式化模型 列控 列车超速防护(ATP) 时段演算(DC) 
一种新的时段演算及其验证被引量：1
《计算机研究与发展》2008年第z1期169-174,共6页梁爱丽 朱嘉奇 王捍贫 屈婉玲 
国家"九七三"重点基础研究发展规划基金项目(2002CB312004);国家"八六三"高技术研究发展计划基金项目(2006AA01Z160)
在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法....
关键词：模型检测 CTL* QDDC NP-完全 
ATP控车模式的DC模型与可靠性分析
《铁道通信信号》2008年第1期39-41,共3页承向军 杜鹏 张春悦 孟令云 
列车控制是保障高速列车安全运行的关键技术。对国际上广泛应用的ATP控车模式建立了基于时段演算的模型,并通过对模型的推演,对ATP控车模式进行了初步的可靠性分析,为设计安全、可靠的ATP系统提供新的理论分析手段。
关键词：列控 列车超速防护 时段演算 可靠性分析 
优先级顶协议的形式化验证
《计算机仿真》2007年第6期276-279,共4页张博颖 
国家863计划项目(2004AA412040);国家自然科学基金项目(60373055;60374058)
优先级顶协议是一种优先级驱动的抢占式调度协议,它具有无死锁和单阻塞的性质。Dang Van Hung和Philip Chan在文献[6]中形式地规范和验证了这两个性质。但他们没有对状态函数HiPripcp明确定义,这使得验证的细节较难理解。为了解决这个问...
关键词：优先级顶协议 时段演算 调度 实时操作系统 形式规范和验证 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部