形式化

作品数：5172被引量：11555H指数：35
导出分析报告
相关领域：自动化与计算机技术文化科学更多>>
相关作者：关永施智平薛锦云张广泉段振华更多>>
相关机构：华东师范大学国防科学技术大学西安电子科技大学清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家社会科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=软件学报x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于TLA+形式化规约的Raft协议测试
《软件学报》2024年第12期5363-5381,共19页王栋 窦文生 高钰 吴陈傲 魏峻 黄涛 
国家自然科学基金(62072444,62302493);国家自然科学基金联合基金(U20A6003)。
Raft是最为流行的分布式共识协议之一.自2014年被提出以来,Raft协议及其变体在各种分布式系统中被广泛应用.为了证明Raft协议的正确性,开发者使用TLA+形式化规约对协议设计进行了建模和验证.但由于抽象的形式化规约与实际的系统实现源...
关键词：RAFT 分布式系统 软件测试 模型检查 
面向物联网设备移动与通信行为的建模及验证
《软件学报》2024年第11期4993-5015,共23页刘靖宇 李晅松 陈芝菲 叶海波 宋巍 
国家自然科学基金(61702263,61761136003);CCF-华为创新研究计划(CCF-HuaweiFM2021004)。
物联网设备的使用范围正在不断扩张.模型检测是提升这类设备可靠性和安全性的有效手段,但常用的模型检测方法不能很好地刻画这类设备常见的跨空间移动和通信行为.为此,提出一种面向物联网设备移动与通信行为的建模及验证方法,以实现对...
关键词：模型检测 物联网 形式化验证 建模语言 
形式化方法与应用专题前言
《软件学报》2024年第9期4011-4012,共2页曹钦翔 宋富 詹乃军 
随着硬件运算速度变得越来越快、体系结构变得越来越复杂,软件的功能也变得越来越强大而复杂,如何开发可靠的软件系统,已经成为了一项巨大的挑战.形式化方法是利用数学理论与方法论证检验软件系统可靠性与安全性的方法,包括模型检验、...
关键词：形式化方法 软件系统 模型检验 运算速度 定理证明 体系结构 应用专题 理论与方法论 
完备神经网络验证加速技术综述
《软件学报》2024年第9期4038-4068,共31页刘宗鑫 杨鹏飞 张立军 吴志林 黄小炜 
中国科学院基础领域研究青年团队计划(CASYSBR-040);中国科学院软件研究所新培育方向项目(ISCAS-PYFX-202201)。
人工智能技术已被广泛应用于生活中的各个领域.然而,神经网络作为人工智能的主要实现手段,在面对训练数据之外的输入或对抗攻击时,可能表现出意料之外的行为.在自动驾驶、智能医疗等安全攸关领域,这些未定义行为可能会对生命安全造成重...
关键词：完备验证 可满足性模理论 人工智能安全 形式化方法 鲁棒性 
舰载机弹药保障作业调度的形式化建模与验证
《软件学报》2024年第9期4100-4122,共23页金钊 金璐 张博闻 吴庆顺 冯朔 李冠峰 徐明亮 
国家自然科学基金(62325602,62302459,62036010,61972362,62372416)。
航母舰载机弹药保障作业的智能规划作为一种高效能航保作业调度方法,是助推航母工程先进技术建设发展的重要途径之一.高安全攸关属性下作业规划方案的正确性保证已经逐渐成为制约其实际应用部署安全的关键技术瓶颈.针对方案正确性验证...
关键词：舰载机弹药保障作业 形式化验证 分离逻辑 操作语义 COQ 
基于MTRDL的自动飞行系统模式需求建模与验证方法被引量：1
《软件学报》2024年第9期4265-4286,共22页徐恒 黄志球 胡军 陶传奇 王金永 石帆 
国家自然科学基金(U2241216);中央高校基本科研业务费专项资金(NT2022027,NJ2022027);河南省科技攻关项目(222102210048)。
在民机自动飞行过程中,自动飞行系统模式转换是影响安全的重要因素,随着现代民机机载系统的功能与复杂度的快速增长,在需求阶段对自动飞行系统模式转换的安全性分析和验证成为重要的挑战.飞行模式转换的复杂性不仅体现在自动飞行过程中...
关键词：自动飞行系统模式 形式化方法 SysML建模 安全性质 
基于DH标定的机器人正向运动学形式化验证被引量：1
《软件学报》2024年第9期4160-4178,共19页谢果君 杨焕焕 石正璞 陈钢 
DH坐标系在机器人运动学分析中发挥着重要的作用.在基于DH坐标系构建的机器人控制系统中,机器人结构的复杂性使得构建安全的控制系统成为一个难题,仅依靠人工方法可能导致系统漏洞和安全风险,从而危及机器人的安全.形式化方法通过演绎...
关键词：机器人运动学 形式化验证 DH坐标系 代码自动生成 
微内核操作系统互斥量模块功能正确性的形式化验证
《软件学报》2024年第9期4179-4192,共14页张林雁 李希萌 施智平 关永 曹钦翔 张倩颖 
国家自然科学基金(62002246,62272322,62272323,62372311,62372312,61902240)。
操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测...
关键词：互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器 
基于形式化方法的区块链系统漏洞检测模型
《软件学报》2024年第9期4193-4217,共25页陈锦富 冯乔伟 蔡赛华 施登洲 Rexford Nii Ayitey SOSU 
国家重点研发计划(2020YFB1005501);国家自然科学基金(62172194,62202206,U1836116);江苏省自然科学基金(BK20220515);中国博士后科学基金(2023T160275);江苏省自然科学基金前沿技术项目(BK20202001);江苏省青蓝工程。
随着区块链技术在各行各业的广泛应用,区块链系统的架构变得越来越复杂,这也增加了安全问题的数量.目前,在区块链系统中采用了模糊测试、符号执行等传统的漏洞检测方法,但这些技术无法有效检测出未知的漏洞.为了提高区块链系统的安全性...
关键词：区块链系统 安全因素 漏洞检测模型 形式化验证 BPEL流程 
共识协议的形式化验证研究现状与展望
《软件学报》2023年第11期4989-5007,共19页葛宁 贺俞凯 翟树茂 李晓洲 张莉 
国家重点研发计划(2018YFB1402700);国家自然科学基金(61902011);北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。
分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格...
关键词：共识协议 形式化验证 限界模型检测 定理证明 布尔表达式可满足性理论 可满足性模理论 
全选清除导出
共15页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部