-
题名基于有限状态进程的事件约束定义
被引量:5
- 1
-
-
作者
顾庆
陈道蓄
谢立
韩杰
孙钟秀
-
机构
南京大学计算机软件新技术国家重点实验室
-
出处
《软件学报》
EI
CSCD
北大核心
2002年第11期2162-2168,共7页
-
基金
国家九五重点科技攻关项目(98-780-01-07-03)~~
-
文摘
测试分布式程序需要定义事件约束来检测程序执行产生的事件序列.事件约束需要根据程序的规约来推导.FSP是一类描述并发程序形式化规约的进程代数记法.它将并发进程描述为动作序列,其中动作可对应到规约级事件.E-CSPE约束在给定状态谓词下定义前后运行事件间的顺序关系.根据FSP的操作符和并发控制机制可推导E-CSPE约束.推导出来的E-CSPE约束考虑到并发程序的安全和进展属性,可据以判断程序运行的正确性和测试的充分性.
-
关键词
有限状态进程
事件约束定义
软件测试
并发程序
软件开发
-
Keywords
software testing
finite state process
specification-based testing
concurrent programs
event sequencing constraints
-
分类号
TP311.52
[自动化与计算机技术—计算机软件与理论]
-
-
题名生成诊断公式的有限状态进程等价验证
被引量:1
- 2
-
-
作者
李明
-
机构
中国科学院软件研究所计算机科学国家重点实验室
中国科学院研究生院
-
出处
《计算机工程与设计》
CSCD
北大核心
2010年第2期344-347,共4页
-
文摘
分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式。算法的时间复杂度为O(mlogn),空间复杂度为O(m+n)。
-
关键词
互模拟
形式验证
带标号的迁移系统
有限状态进程
Hennessy-Milner逻辑
-
Keywords
bisimulation
forma
verification
labeled transition system
finite state processes
Hennessy-Miluer logic
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
-
题名基于体系结构的信息物理融合系统的研究与分析
被引量:1
- 3
-
-
作者
梁刚强
张立臣
-
机构
广东工业大学计算机学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2016年第6期1371-1376,共6页
-
基金
国家自然科学基金项目(61370082)资助
国家自然科学基金项目(61173046)资助
-
文摘
提出一种对现有软件体系结构的扩展来满足复杂的信息物理融合系统(CPS)的建模需求,增加对CPS的物理系统、物理系统的的联系交互、物理系统和信息系统之间交互的建模支持.首先引入一种新的CPS体系结构模式来对整个系统架构进行描述和构建,并以此作为原型设计和对使用基于模型工具创建的设计替代方案进行分析评价的参考环境.文章提出的CPS体系结构模式在Acme Studio中进行实现,并且对组件和连接器做了行为解释,这些行为解释通过以标签转换系统分析器(LTSA)作为扩展插件的有限状态进程(FSP)或者以多面混合自动机验证机(PHAVer)作为扩展插件的线性混合自动机(LHA)进行验证.最后,文章用一个锅炉温度控制系统的实例来解释提出的CPS体系结构模式和所用到的分析插件.
-
关键词
体系结构描述语言
信息物理融合系统
CPS体系结构模式
有限状态进程
线性混合自动机
-
Keywords
architecture description language
cyber-physical systems
CPS architecture style
finite state process
linear hybrid automata
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-
-
题名基于ADL的物理信息系统的建模与分析
被引量:1
- 4
-
-
作者
柳求金
张立臣
-
机构
广东工业大学计算机学院
-
出处
《计算机技术与发展》
2012年第4期104-107,共4页
-
基金
国家自然科学基金重大研究计划(90818008)
国家自然科学基金项目(60774095
+2 种基金
60474072Z)
广东省自然科学基金项目(07001774
04009465)
-
文摘
当前分析和设计物理信息系统的模型和方法通常是线性分离的,且由不同的数学形式化方法和工程与计算机科学中的不同方法定义。为便于处理,对关注点分离是必要的,但这种分析方式由于在系统设计时过早地将系统信息特征与物理特征分离,导致很难评估直接与这两个领域进行交互的可替换元素的影响和协调性。文中对围绕组成CPS系统的所有范围的元素的架构描述进行扩展,最终目的是能够建立一个可扩展的框架,包括一套可被创建的综合设计工具。由此文中提出这种物理信息系统建模方法并通过一个简单应用实例对方法进行说明。
-
关键词
体系结构描述语言
物理信息系统
有限状态进程
线性混合自动机
-
Keywords
architecture description languages
cyber-physical systems
finite state processes
linear hybrid automata
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-