形式规格说明

作品数：16被引量：36H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：缪淮扣文志诚李晓博陈怡海许庆国更多>>
相关机构：上海大学西北大学中国石油大学（华东）江西师范大学更多>>
相关期刊：《西北大学学报（自然科学版）》《科技信息》《计算机应用与软件》《计算机应用研究》更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划国家高技术研究发展计划湖南省教育厅科研基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
Radl形式规格说明相对正确性研究被引量：6
《软件学报》2013年第4期715-729,共15页王昌晶 薛锦云 
国家自然科学基金重大国际(地区)合作与交流项目(61020106009);国家自然科学基金(61272075);江西省自然科学青年科学基金(201222BAB211030)
在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者...
关键词：形式规格说明 相对正确性 确认 扩展的逻辑系统 辅助证明算法 
用带时钟变量的线性时态逻辑扩充Object-Z被引量：1
《计算机应用研究》2009年第5期1764-1769,共6页文志诚 李长云 满君丰 
国家自然科学基金资助项目(60773110);湖南省教育厅科研项目(08c284;08c286)
Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首...
关键词：OBJECT-Z 用带时钟变量的时态逻辑 实时系统 形式规格说明 形式验证 
形式化方法自动生成测试用例的算法研究被引量：1
《科技信息》2008年第23期73-74,共2页王冬 吕慧娟 
本文提出了一种从形式规格说明中利用等价类划分的方法自动生成软件测试用例的算法,给出了算法步骤.算法设计,并进行了算法分析。最后指出了下一步工作的重点所在。
关键词：形式化方法 测试用例 等价类划分 形式规格说明 
基于形式规格说明和分类树方法生成软件测试用例被引量：5
《微计算机应用》2007年第4期411-414,共4页朱连章 马桂真 
介绍了一种基于形式规格说明和分类树方法生成软件测试用例的方法。由软件的形式规格说明构造分类树,再把由分类树方法得到的测试用例转化为析取范式,进一步精炼测试用例。并通过一个实例说明测试用例的设计过程。
关键词：测试用例 规格说明 分类树方法 
网络实时系统的一种活动性描述语言
《计算机应用研究》2007年第4期288-291,共4页彭伟洁 张立臣 
国家自然科学基金资助项目(60474072;60174050);广东省自然科学基金资助项目(04009465;010059);广东省高校自然科学基金资助项目(Z03024)
介绍了ADL,它是一种基于网络实时系统的活动性描述语言,一种描述并发处理中时态和功能行为的新的形式规格说明符号。ADL专用于计算机网络,是DOR IS的一种形式语言扩充。它组合了状态机活动(ASM)的图形符号和基于模型的活动功能行为(AFB...
关键词：结构描述语言 形式规格说明 实时处理 
实时系统形式规格说明在PVS中的建立被引量：1
《计算机科学》2006年第12期238-242,共5页许庆国 缪淮扣 
国家自然科学基金项目(批准号60173031);国家973项目(编号:2002CB312001)资助。
本文首先简介了时间自动机和时间B櫣chi自动机形式模型,结合时间化时序逻辑(TimedTemporalLogic)的语法和语义,利用定理证明器PVS(PrototypeVerificationSystem)实现了定义在时间自动机状态(或运行)上的时间化分支(或线性)时序逻辑规格...
关键词：实时系统 时间Büchi自动机 时间化时序逻辑 PVS 
一种从Object-Z到CSP规格说明的转化方法
《计算机科学》2006年第11期263-267,共5页文志诚 缪淮扣 许庆国 
国家自然科学基金(60373072);上海市教委第四期重点学科建设基金资助。
面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化...
关键词：Object—Z CSP 形式规格说明 参数化进程 转化 
基于形式规格说明的构件匹配被引量：4
《计算机应用与软件》2006年第10期10-12,73,共4页李晓博 缪淮扣 刘静 
国家自然科学基金(60373072)资助
构件匹配依靠精确描述构件的语义,而形式规格说明基于严格的数学概念和理论。将两者结合起来,首先利用Z语言描述属性、方法和构件的类型,并在此基础上,通过一个例子,给出了各种匹配机制的公理描述。最后,介绍了构件匹配的一个重要应用...
关键词：形式规格说明 构件匹配 构件检索 
Z规格说明的测试用例自动生成
《应用科学学报》2006年第4期377-381,共5页朱彬 缪淮扣 王娜 
国家自然科学基金资助项目(60373072)
软件测试是软件质量保证的重要手段,测试用例的生成是软件测试的关键和难点.文中应用范畴划分测试方法产生测试框架,并引入线性规划模型,通过构造线性规划模型来实例化测试框架,并且较好地解决了测试框架是否可行的判断问题.同时结合票...
关键词：范畴划分测试 测试用例 线性规划 形式规格说明 Z 
Object-Z规格说明的结构模拟动画技术被引量：4
《上海大学学报（自然科学版）》2005年第6期589-595,共7页朱江 陈怡海 缪淮扣 
国家自然科学基金资助项目(60373072);上海市教委科学技术发展基金资助项目(02AK07)
形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一...
关键词：形式方法 形式规格说明 确认 动画模拟 OBJECT-Z PROLOG SICStus PROLOG 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部