形式化方法

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程与设计x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于SPIN的HMSC模型自动检验方法
《计算机工程与设计》2023年第10期3047-3055,共9页李立亚 孙雨荷 马汉杰 丁佐华 黄鸿云 
国家自然科学基金项目(62132014)。
自动检测与验证HMSC(high-level message sequence chart)模型的正确性对保证文本需求被正确建模具有十分重要的意义,为此提出一种为HMSC模型进行自动检验的方法,并将其实现。利用转换规则为HMSC模型生成Promela检测语言,借助SPIN工具...
关键词：模型检测 HMSC模型 SPIN工具 正确性验证 模型转换 Promela语言 形式化方法 
基于时序约束建模的自动精化和组合工具
《计算机工程与设计》2021年第7期2077-2086,共10页王烨凯 苏雯 
国家自然科学基金项目(61602293)。
为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法。开发对应的自动精化和组合的工具...
关键词：形式化方法 混合系统 时序约束建模 自动精化和组合方法 自动精化和组合工具 
机载系统的功能研制保证等级验证方法被引量：1
《计算机工程与设计》2021年第3期867-874,共8页蒋泉 朱春玲 王旭亮 尹小花 
国家自然科学基金重点基金项目(11832012)。
为保证机载系统研制过程中人为分配的功能研制保证等级是合理的,提出一种机载系统功能研制保证等级的验证方法。考虑不同架构设计对系统功能研制保证等级分配的影响,结合模型驱动和形式化方法,研究系统的功能研制保证等级与安全标准的...
关键词：机载系统 功能研制保证等级 形式化方法 安全标准 系统安全性 
面向业务的动态任务分配工作模型定义
《计算机工程与设计》2014年第8期2960-2964,共5页李春芳 徐建军 
湖南省科技计划基金项目(2010GK3068)
为解决面向业务的完整动态任务分配工作模型缺失以及组成内容之间工作关系语义不清晰的问题,提出策略优先的动态任务分配工作模型S-DTAWM。利用集合论的描述语言,形式化定义S-DTAWM各构件内容、工作关系及执行算法,为面向业务的通用动...
关键词：面向业务 完整动态任务分配工作模型 策略优先 S-DTAWM 形式化方法 构件 
基于Z规格的UML模型形式化转换及验证
《计算机工程与设计》2013年第6期2031-2035,共5页张杨 段富 
山西省自然科学基金项目(2008011039);山西省科技攻关基金项目(20080322008)
统一建模语言(UML)所建立的模型的正确性无法通过其本身进行形式化验证,为解决这个问题,根据UML模型的静态性质和动态模块行为两个方面提出结合形式化规格说明语言的模型形式化方案,以此为基础提出将UML目标模型转化为Z规格说明的形式...
关键词：形式化方法 形式化验证 统一建模语言 Z规格 Z-EVES 
基于Hoare逻辑的过程调用的形式化方法被引量：2
《计算机工程与设计》2011年第1期197-201,共5页雷富兴 张来顺 
采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这...
关键词：HOARE逻辑 过程语义 过程调用语义 前置条件 后置条件 
循环条件的形式化推导在程序验证中的应用被引量：1
《计算机工程与设计》2010年第14期3193-3197,共5页雷富兴 张来顺 石荣刚 杨科 
提出了一种求解命令式程序中循环执行和终止条件的方法。该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导。现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序。提出...
关键词：循环执行 循环终止 形式化方法 自动化 程序验证 缺陷修正 
大型复杂协议的形式化分析方法研究
《计算机工程与设计》2009年第18期4207-4210,共4页赵娟 韩继红 王亚弟 黄卿 
大型复杂协议的形式化分析是目前研究的一个热点和难点。根据所采用技术的特点,将大型复杂协议的形式化分析方法分为基于逻辑推理的方法、基于模型检测的方法、基于定理证明的方法和基于进程代数的方法,并简要介绍了各类方法的代表性方...
关键词：大型复杂协议 形式化方法 逻辑推理 模型检测 定理证明 进程代数 
基于PEPA的组合服务性能建模与分析被引量：1
《计算机工程与设计》2009年第19期4579-4580,F0003,共3页方光伟 甘诚智 郑啸 
安徽省高校省级自然科学研究基金项目(KJ2007B308ZC)
当前对于组合服务的分析主要侧重在功能方面,缺乏有效地进行性能分析的手段和工具。针对此问题,提出一种基于PEPA(performance evaluation process algebra)的组合服务性能建模与评价方法。基于服务组合图对组合服务中原子服务的交互行...
关键词：服务组合 性能评价进程代数 性能建模 性能分析:形式化方法 
基于形式化方法的测试驱动开发研究被引量：6
《计算机工程与设计》2008年第15期3944-3946,3950,共4页刘振宇 王恒 
湖南省自然科学基金项目(60073003);湖南省教育厅基金项目(4-02-JY-02C371)
对测试驱动开发中测试用例的自动生成和管理问题进行了研究,并对现有方法进行了分析和比较。给出了一种基于形式化方法的测试用例生成和管理方案。该方案通过形式化语言描述软件规约,并通过相应工具生成和管理测试用例,从而提高了测试...
关键词：极限编程 形式化方法 测试驱动开发 软件过程 软件重构 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部