形式化方法

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机科学x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种基于变量隐藏抽象的IC3硬件验证算法
《计算机科学》2023年第S02期783-788,共6页杨柳 范洪宇 李东方 贺飞 
国家重点研发计划课题(2018YFB1308601);国家自然科学基金(62072267,62021002);国防基础科学科研计划(XX2020204B028)。
随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。...
关键词：硬件验证 IC3算法 形式化方法 模型检验 变量隐藏抽象 
基于CPN的供应链合约的形式化验证被引量：1
《计算机科学》2023年第S01期707-713,共7页郑红 钱诗慧 刘泽润 杜渂 
2019年度上海市信息化发展(大数据发展)专项资金项目(201901043)。
智能合约的安全性对于区块链在供应链领域的应用尤为重要。目前,大多数对智能合约的形式化验证工作集中于漏洞检测,对于如何在部署上链前生成安全的智能合约的关注仍然比较少,如何有效规范地将特定领域的属性安全地映射为智能合约代码...
关键词：智能合约 形式化方法 模型检查 CPN 供应链 
设计模式组合操作优化研究被引量：3
《计算机科学》2020年第3期19-24,共6页纪程宇 朱雪峰 
国家自然科学基金(60496324);中国石油大学科研基金(KYJJ2012-05-17) ~~
作为软件设计经验的总结,恰当使用设计模式能够有效提高软件系统的可复用性,确保最终所得软件产品的质量。但在实际应用中,人们很少使用单一的设计模式,通常需要根据实际的应用场景进行多个模式的组合,这可能会导致所得结果不确定,严重...
关键词：设计模式 模式组合 操作优化 形式化方法 等式推理 
基于Coq记录的矩阵形式化方法被引量：5
《计算机科学》2019年第7期139-145,共7页马振威 陈钢 
南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20171610);中央高校基本科研业务费专项资金资助
矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数...
关键词：COQ 矩阵 形式化验证 定理证明 记录类型 
支持抽象解释的静态分析方法的形式化体系研究
《计算机科学》2017年第12期126-130,155,共6页张弛 黄志球 丁泽文 
国家高技术研究发展计划(863)(2015AA105303);国家自然科学基金资助项目(61272083);软件新技术与产业化协同创新中心资助
在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable ...
关键词：形式化方法 静态分析 抽象解释 可配置程序分析 
一种面向SaaS多租户的多层模型被引量：8
《计算机科学》2017年第11期56-63,共8页李响 李彤 谢仲文 何云 成蕾 韩煦 
国家自然科学基金(61379032;61262024;61462092);云南省教育厅科学研究基金(2014Y012)资助
SaaS(Software as a Service)伴随云计算而出现,它与传统软件的区别较大。根据SaaS软件的特点,提出支持SaaS软件成熟度的SaaS软件分层元模型,使用形式化方法对每一层进行建模描述。受面向对象Petri网(ObjectOriented Petri Nets,OOPN)...
关键词：形式化方法 PETRI网 SAAS 软件建模 
面向系统能力的形式化分析和测试方法被引量：1
《计算机科学》2017年第S1期534-538,共5页陈平 梁启明 孙伟 
核高基国家科技重大专项(JAZ1472010)资助
国内软件业界实施系统测试时,大部分采用对系统规格说明描述的功能点进行逐一测试的方法,很少从系统能力的角度进行测试,难以充分说明系统软件产品满足系统能力需求的要求。同时,系统规格说明使用自然语言进行描述,存在语义不准确的现象...
关键词：系统测试 系统能力测试 形式化方法 软件需求分析 
电力智能单元传输规约安全性分析模型研究
《计算机科学》2016年第S2期329-337,共9页马媛媛 陈喆 汪晨 费稼轩 黄秀丽 
国家电网公司项目:电网智能化单元传输规约安全分析及增强技术研究资助
电力智能单元传输规约的安全性是保障智能电网中智能通信实现高速、可靠、安全的基础。为了构建适用于电力智能单元传输规约的安全性分析模型,概述了主流的协议安全性分析理论与方法。基于符号模型的形式化方法包括逻辑推理、模型检验...
关键词：协议安全性分析 符号模型 计算模型 计算可靠的形式化方法 电力智能单元传输规约 
面向DO-333的襟缝翼控制单元安全性分析被引量：6
《计算机科学》2016年第5期150-156,161,共8页陈光颖 黄志球 陈哲 阚双龙 
国家自然科学基金(61100034;61170043);中国博士后科学基金(20110491411);江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助
DO-333是对机载软件安全性标准DO-178C关于形式化方法的补充,为机载软件开发过程中形式化方法的使用提供指导。模型检验作为一种形式化方法,可以应用于对软件需求和设计阶段制品的严格验证。基于DO-333,使用模型检验对飞控系统中襟缝翼...
关键词：适航认证 形式化方法 模型检验 机载软件 SPIN 
连续傅里叶变换基础理论的高阶逻辑形式化被引量：2
《计算机科学》2015年第4期31-36,共6页吕兴利 施智平 李晓娟 关永 叶世伟 张杰 
国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(60873006;61070049;61170304;61104035;61373034;61303014);北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028 036);北京市优秀人才培养项目;北京市属高校青年拔尖人才培育计划资助
连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用。利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相...
关键词：形式化方法 定理证明 连续傅里叶变换 HOL4 频率响应 
全选清除导出
共6页<123456>
检索报告 对象比较 聚类工具 使用帮助 返回顶部