-
题名从活性顺序图到时态逻辑的转化方法
被引量：2
- 1
-
-
作者
付明慧
周清雷
张兵
-
机构
郑州大学信息工程学院
-
出处
《计算机工程与设计》
CSCD
北大核心
2012年第9期3437-3441,共5页
-
基金
国家863高技术研究发展计划基金项目(2007AA010408)
-
文摘
为了将活性顺序图用于模型检测,方便描述系统的场景需求,提出了一种将活性顺序图转换成时态逻辑的转化方法。分析活性顺序图语言并且定义一种基于路径的语义,用活性顺序图表述系统的场景需求。根据提出的语义,给出了一个将场景需求显式转化为时态逻辑的一般方法,针对并发消息较多的系统扩展和优化此方法,以得到更简短的时态逻辑公式。通过实例说明活性顺序图到线性时态逻辑的转化过程。
-
关键词
活性顺序图
时态逻辑
路径语义
场景需求
模型检测
-
Keywords
LSC
temporal logic
trace-based semantics
scenarios requirement
model checking
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名基于活性顺序图的形式化验证方法及工具研究
被引量：1
- 2
-
-
作者
张坤
叶俊民
王嫱
赵丽娴
陈曙
-
机构
华中师范大学计算机学院
-
出处
《计算机测量与控制》
2016年第5期274-278,共5页
-
基金
国家科技支撑计划项目(2015BAK33B00)
教育部规划基金项目(15YJA880095)
中央高校基本科研业务费专项资金科研项目(CCNU15GF003)
-
文摘
近年来,形式化验证方法在软件开发过程的作用越来越大;如何充分利用形式化验证方法提高软件系统的可靠性已成为软件开发者及使用者主要关注的问题;总结了近年来基于活性顺序图的形式化验证方法的研究进展,首先介绍活性顺序图的语言及其表达能力与复杂性,然后深入分析现有的基于活性顺序图的形式化验证的关键技术及其典型应用,最后实现一种基于活性顺序图的运行时验证工具,实验证明使用本验证工具进行形式化验证的可行性。
-
关键词
活性顺序图
形式化验证
软件开发过程
-
Keywords
live sequence chart
formal verification
software development process
-
分类号
TP393
[自动化与计算机技术—计算机应用技术]
-
-
题名一种基于活性顺序图的运行时验证研究
被引量：1
- 3
-
-
作者
叶俊民
张坤
叶竹君
陈盼
陈曙
-
机构
华中师范大学计算机学院
华中师范大学国家物理学人才培养基地
-
出处
《计算机科学》
CSCD
北大核心
2016年第8期137-141,164,共6页
-
基金
国家科技支撑计划项目(2015BAK33B00)
中央高校基本科研业务费专项资金科研项目(CCNU15GF003)
教育部人文社会科学研究规划基金(15YJA880095)资助
-
文摘
运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重写逻辑验证算法效率较低等问题,提出一种基于活性顺序图的运行时验证的改进方法,以支持现有的运行时验证技术。实验表明,改进方法验证结果准确,且验证过程开销较小。
-
关键词
活性顺序图
线性时序逻辑
重写逻辑
运行时验证
-
Keywords
Live sequence chart, Linear temporal logic,Rewriting logic, Runtime verification
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
