形式化方法

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于状态图转形式化B模型的安全苛求系统开发方法
《计算机工程》2024年第11期173-186,共14页赵大地 王恪铭 
四川省自然科学基金(2022NSFSC0464);成都市软科学研究项目(2023-RK00-00084-ZF)。
形式化方法精确且严格,较多应用于安全苛求系统开发,但目前仍存在学习成本高、使用复杂、重用性低等问题。常用的非形式化状态图模型虽易于使用却缺乏严格验证。针对这些问题,提出一种将状态图SCXML模型转译为形式化B模型的模型转化方法...
关键词：软件功能安全 形式化方法 模型转化 SCXML状态图 B方法 
基于强化学习的安全协议形式化验证优化研究被引量：3
《计算机工程》2021年第12期141-146,共6页杨锦翔 熊焰 黄文超 
国家重点研发计划(2018YFB2100300,2018YFB0803400);国家自然科学基金(61972369,61572453,61520106007,61572454);中央高校基本科研业务费专项资金(WK2150110009)。
使用形式化方法能够找到安全协议设计中存在的漏洞,但高效地对安全协议进行自动的形式化分析仍然是一个挑战。针对现有形式化自动验证工具无泛化性和效率低的不足,对基于强化学习的安全协议形式化验证框架smartVerif进行优化。使用无人...
关键词：强化学习 安全协议 形式化方法 自动验证 泛化性 
轨道交通控制软件中基于场景的需求分析方法被引量：1
《计算机工程》2021年第8期284-293,300,共11页闫倩倩 缪炜恺 
国家自然科学基金面上项目“数据驱动的机器学习软件系统的形式化需求建模工程方法”(61872144);国家自然科学基金青年基金“嵌入式控制软件的形式化规格说明构建的工程方法”(61402178)。
针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供...
关键词：形式化方法 需求规约 需求确认和验证 场景优化 轨道交通控制软件 
基于Event-B的自动化模块组合方法研究被引量：1
《计算机工程》2019年第5期298-307,314,共11页陈金鑫 苏雯 
国家自然科学基金(61602293)
Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用...
关键词：形式化方法 Event-B方法 模块化建模 自动化模块组合方法 模块调用 精化 
基于改进Event-B建模的高速列车追踪运行仿真研究被引量：3
《计算机工程》2015年第8期256-261,共6页陈永 张薇 胡晓辉 
国家自然科学基金资助项目(61163009);兰州交通大学青年科学基金资助项目(2011001)
针对铁路移动闭塞系统中高速列车间隔动态实时变化的特征,结合Agent理论对Event-B方法中Machine动态属性进行改进,提出一种基于Event-B建模方法的高速列车追踪运行模型。给出高速列车追踪运行形式化控制策略,研究运行过程中速度变化关...
关键词：高速列车 列车追踪 Event-B方法 形式化方法 交通仿真 建模 
CTCS-2级列控系统的形式化建模与验证被引量：1
《计算机工程》2013年第3期12-15,共4页董昱 水晶 黎磊 
国家自然科学基金资助项目(61164010);甘肃省教育厅硕导基金资助项目(210110)
由于CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使...
关键词：列控系统 符号模型检验 形式化方法 车载设备 模式转换 
基于范畴论的构件行为组合研究被引量：4
《计算机工程》2012年第15期53-55,58,共4页赵硕 陈中育 肖春水 
浙江省科技计划基金资助重点项目(2007C23087);浙江省自然科学基金资助项目(LY12F02009)
针对基于构件开发过程中单个构件功能难于满足用户需求的问题,提出一种利用范畴论对构件行为进行组合的方法,用以实现复杂的业务功能。采用范畴论给出构件的形式语义描述,构件与构件之间的行为交互关系采用图表进行建模。给出一种基于...
关键词：范畴论 图表 形式化方法 构件行为 构件组合 推出 
基于模型检测的系统生存性分析被引量：2
《计算机工程》2012年第17期38-41,共4页周清雷 张兵 席琳 
国家"863"计划基金资助项目"基于ASP模式的软件服务支持技术研究"(2007AA010408)
提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PR...
关键词：生存性分析 形式化方法 模型检测 PRISM检测工具 离散马尔科夫链 概率计算树逻辑 
软件体系结构的广义视角研究被引量：2
《计算机工程》2012年第23期42-46,共5页马苏拉 
云南省应用基础研究基金资助项目(2006F0047M);云南财经大学人才引进研究基金资助项目
从广义视角出发,将一些独立发展的软件领域归结到软件体系结构(SA)领域,包括UML、面向方面程序设计、面向服务体系结构、基于构件的软件工程。考虑它们之间的相互联系、共同性和独特性,给出一种分类框架。指出软件体系结构的发展方向:S...
关键词：分类框架 构件 形式化方法 面向对象 软件体系结构 软件工程 
基于时间自动机的嵌入式系统调度分析工具被引量：1
《计算机工程》2012年第3期290-292,共3页于淼 李允 桂盛霖 罗蕾 
国家自然科学基金资助项目(90718019);国家"863"计划基金资助项目(2007AA010304)
为验证嵌入式实时系统开发过程中任务集的可调度性,设计并实现一种嵌入式系统调度分析工具。提出通用任务模型,建立任务与事件到达自动机和任务状态自动机的状态关系映射,利用基于模型检测的时间自动机可达性方法判定系统的可调度性。...
关键词：形式化方法 时间自动机 可调度性 嵌入式实时系统 任务模型 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部