形式化方法

作品数：863被引量：2365H指数：18
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：薛锦云肖美华张广泉黄志球胡军更多>>
相关机构：华东师范大学中国科学院软件研究所上海交通大学南京大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划中央高校基本科研业务费专项资金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机应用x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于线性误差断言的推理方法被引量：1
《计算机应用》2021年第8期2199-2204,共6页武鹏 吴尽昭 
国家自然科学基金资助项目(61772006)。
误差在系统中是普遍存在的。在安全关键系统中,对误差的定量分析是必要的,而以往的推理验证方法较少考虑误差。误差通常用区间数来刻画,从而推广了线性断言,并给出了线性误差断言的概念。此外,结合凸集的性质,提出了求解线性误差断言顶...
关键词：形式化方法 定理证明 推理方法 蕴含关系 误差理论 
基于系统理论过程分析的软件安全性需求分析与验证方法被引量：2
《计算机应用》2020年第11期3261-3266,共6页秦楠 马亮 黄锐 
国家自然科学基金资助项目(51377169)。
针对传统系统理论过程分析(STPA)方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描...
关键词：系统理论过程分析 软件安全需求 形式化方法 模型检验 武器发射控制系统 
基于离散控制器合成的异构多核系统资源管理方法被引量：6
《计算机应用》2020年第6期1698-1706,共9页安鑫 夏近伟 杨海娇 欧阳一鸣 任福继 
国家自然科学基金青年基金资助项目(61502140);国家自然科学基金联合基金资助项目(U1613217);中央高校基本科研业务费专项资金资助项目(JZ2020YYPY0092)。
近年来,随着半导体技术的发展以及应用多样化的需求,异构多核处理器已被广泛应用于高性能嵌入式系统中。这类系统面临的一个主要挑战就是如何在运行时对系统的可用资源(包括处理核等)进行管理分配从而满足系统及其所运行应用在性能和功...
关键词：异构多核处理器 资源管理 形式化方法 离散控制器合成 模型检测 
基于一种形式化方法的3D虚拟祭祀场景建模语言与环境
《计算机应用》2018年第9期2666-2672,2711,共8页徐晓丹 李秉杰 李伯森 吕舜 
财政部重大专项(1181501100001)~~
针对现有三维(3D)场景建模方法普遍存在着业务耦合度高,复杂场景对象属性和特征描述能力不强、不丰富,不能很好地解决3D虚拟祭祀场景建模的问题,提出了基于一种形式化方法的场景建模语言与建模环境。首先,通过引入场景对象、场景对象模...
关键词：3D建模 虚拟祭祀 祭祀场景 建模环境 形式化 
自适应软件动态过程时间特性建模与验证方法被引量：4
《计算机应用》2018年第3期799-805,共7页韩德帅 邢建春 杨启亮 李决龙 
江苏省自然科学基金资助项目(BK20151451)~~
现有自适应软件建模与验证方法较少考虑时间约束,然而,在时间攸关应用领域,自适应软件能否正确运行,不仅要考虑自适应逻辑的正确性,还要考虑自适应软件动态过程的时间特性。为此,首先显式定义了自适应软件的时间特性(监控周期、延迟触...
关键词：自适应软件 时间特性 形式化方法 时间自动机 模型检验 
改进的OpenID Connect协议及其安全性分析被引量：5
《计算机应用》2017年第5期1347-1352,共6页鲁金钿 尧利利 何旭东 孟博 
国家自然科学基金资助项目(61272497);湖北省自然科学基金资助项目(2014CFB249)~~
Open ID Connect协议是最新的单点登录协议之一,已经广泛应用于用户身份认证领域,其安全性受到了人们的重点关注。为增强Open ID Connect协议的安全性,首先引入数字签名及非对称加密技术,对其进行改进,重点关注改进后协议的秘密性和认证...
关键词：非对称加密 数字签名 认证性 符号模型 形式化方法 Pro Verif 
不可满足子式在谓词抽象中的应用与分析
《计算机应用》2014年第A01期273-276,共4页张建民 黎铁军 张峻 庞征斌 李思昆 
国家863计划项目(2012AA01A301);国家自然科学基金资助项目(61103083;61133007)
随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少...
关键词：功能验证 形式化方法 谓词抽象 布尔可满足性 最小不可满足子式 
方块苗文动态构造方法的形式化描述被引量：2
《计算机应用》2014年第3期861-864,868,共5页莫礼平 周恺卿 
国家自然科学基金资助项目(61363033)
针对如何在计算机中生成和显示方块苗文的问题,提出了一种方块苗文动态构造方法,给出了该方法的基本原理,定义了实现方块苗文动态构造所需要的操作符,并以谓词规则的形式对方块苗文动态构造变换操作进行了描述。该方法仅需存储方块苗文...
关键词：方块苗文 信息处理技术 形式化方法 上下文无关文法 谓词规则 
基于梯形逻辑的联锁系统形式化验证方法被引量：4
《计算机应用》2013年第12期3419-3422,3431,共5页于丽贞 徐中伟 陈祖希 张舒青 
国家自然科学基金资助项目(60674004);国家863计划项目(2012AA112801)
铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL)...
关键词：铁路联锁系统 模型检测 形式化方法 梯形逻辑 NuSMV模型检测 
云计算环境中结构化文档形式化建模被引量：2
《计算机应用》2013年第5期1267-1270,共4页熊金波 姚志强 金彪 
福建省自然科学基金资助项目(2011J01339);福建省教育厅科技项目(JA12078;JB12022;JB11034)
结构化文档是云计算环境中实现信息交互与传播的载体,针对已有研究工作缺乏能够描述这种载体的结构化文档模型的问题,在深入分析云计算环境中结构化文档特征的基础上,对文档元素、原子文档元素、连接、文档片段、复杂文档元素等进行形...
关键词：云计算 结构化文档模型 形式化方法 文档元素 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部