裴玉

作品数：2被引量：0H指数：0
导出分析报告
供职机构：南京大学更多>>
发文主题：混成系统反应式系统测试用例SPIN《社会契约论》更多>>
发文领域：自动化与计算机技术哲学宗教更多>>
发文期刊：《计算机研究与发展》《软件学报》更多>>
所获基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-2
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
QRDChecker:一个QRDC模型检验工具
《软件学报》2005年第3期355-364,共10页裴玉 徐启文 李宣东 郑国梁 
国家自然科学基金;国家重点基础研究发展规划(973)~~
反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如 LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可...
关键词：模型检验 有限性性质 反应式系统 时段时序逻辑 
LDPChecker——一个实时和混成系统模型检验工具
《计算机研究与发展》2005年第1期38-46,共9页裴玉 李宣东 郑国梁 
国家自然科学基金项目(60073031;60233020)国家"八六三"高技术研究发展计划基金项目(2001AA113203)国家"九七三"重点基础研究发展规划基金项目(2002CB312001)江苏省自然科学基金项目(BK2001033)
混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机,其对于线性时段性质的满足性能够通过...
关键词：实时和混成系统 混成自动机 线性时段性质 模型检验 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部