-
题名时间属性序列图:语法和语义
被引量:5
- 1
-
-
作者
张鹏程
李必信
李雯睿
-
机构
东南大学计算机科学与工程学院
河海大学计算机与信息学院
-
出处
《软件学报》
EI
CSCD
北大核心
2010年第11期2752-2767,共16页
-
基金
国家自然科学基金Nos.60773105
60973149
+1 种基金
国家高技术研究发展计划(863)No.2008AA01Z113
中央高校基本科研业务费专项资金No.2009B04314~~
-
文摘
为了表示事件出现的时间约束,扩展属性序列图为时间属性序列图,使其继承属性序列图的优点,并且能够表示时间属性,定义了时间属性序列图的形式语法,并给出基于时间Büchi自动机的形式操作语义;用实时规约模式度量了时间属性序列图的表达力.最后,对时间属性序列图进行了实例研究,显示了其广泛的应用前景.
-
关键词
属性序列图
时间属性序列图
时间Büchi自动机
形式验证
-
Keywords
property sequence chart; timed property sequence chart; timed Büchi automaton; formal verification;
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于时间属性序列图的监控器构造方法
- 2
-
-
作者
叶俊民
辜剑
陈曙
董威
舒绍娴
-
机构
华中师范大学计算机学院
国防科技大学计算机学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2015年第7期1426-1431,共6页
-
基金
国家"九七三"重点基础研究发展计划课题项目(2014CB340703)资助
-
文摘
运行时验证一般采用时态逻辑来描述要验证的需求规约,并根据需求规约构造监控器.这对于那些没有形式化经验的软件工程师而言,是一件非常困难的事情,同时,这类方法通常缺少时间机制支撑,因此难以满足实时系统运行时验证中的要求.序列图得到了广泛使用,研究基于序列图来自动生成监控器就显得十分有意义.提出基于UML2.0时间属性序列图的监控器的自动生成方法,其具体思想是使用时间属性序列图来描述要验证的需求规约,然后将整个序列图转换为时间自动机网络,构造出监控器.实验表明,该方法方便缺少形式化经验的软件工程师使用,所产生的监控器运行开销较小,能满足验证对实时性的要求,且有效缓解了监控器生成过程中的组合爆炸.
-
关键词
时间属性序列图
时间自动机
监控器
运行时验证
-
Keywords
timed property sequence diagram
timed automaton
monitor
runtime verification
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名试验性股票指数的建立
被引量:1
- 3
-
-
作者
喻思慧
-
机构
长沙理工大学
-
出处
《品牌》
2015年第12期196-,共1页
-
文摘
在股票市场里,上证指数涨跌情况和走向趋势是投资者们做出决策时最重要的依据之一。然而很多时候它显示出来的数据都存在着一些"失真"的现象,更是难以发挥经济"晴雨表"的功能。笔者深入分析之后发现了上证指数的编制中存在一些不科学合理之处,希望借此引起有关部门重视,并且尝试引进成交量要素和时间序列属性,为上证指数的完善提供思路。
-
关键词
上证指数
成交量
权重
时间序列属性
-
分类号
F832.51
[经济管理—金融学]
-