计算机应用 ›› 2018, Vol. 38 ›› Issue (3): 799-805.DOI: 10.11772/j.issn.1001-9081.2017081992

• 计算机软件技术 • 上一篇    下一篇

自适应软件动态过程时间特性建模与验证方法

韩德帅1, 邢建春1, 杨启亮1,2, 李决龙3   

  1. 1. 陆军工程大学 国防工程学院, 南京 210007;
    2. 清华大学 土木工程系, 北京 100084;
    3. 海军海防工程研究中心, 北京 100841
  • 收稿日期:2017-08-15 修回日期:2017-09-19 出版日期:2018-03-10 发布日期:2018-03-07
  • 通讯作者: 韩德帅
  • 作者简介:韩德帅(1990-),男,山东聊城人,博士研究生,CCF会员,主要研究方向:软件自适应、信息物理系统;邢建春(1964-),男,河北石家庄人,教授,博士生导师,博士,主要研究方向:信息物理系统、建筑信息模型;杨启亮(1975-),男,河南信阳人,副教授,博士,主要研究方向:软件自适应、建筑信息模型;李决龙(1959-),男,安徽安庆人,教授,博士生导师,硕士,主要研究方向:建筑环境与设备工程。
  • 基金资助:
    江苏省自然科学基金资助项目(BK20151451)。

Modeling and verification approach for temporal properties of self-adaptive software dynamic processes

HAN Deshuai1, XING Jianchun1, YANG Qiliang1,2, LI Juelong3   

  1. 1. College of Defense Engineering, Army Engineering University of PLA, Nanjing Jiangsu 210007, China;
    2. Department of Civil Engineering, Tsinghua University, Beijing 100084, China;
    3. Research Center of Coastal Defense Engineering, Beijing 100841, China
  • Received:2017-08-15 Revised:2017-09-19 Online:2018-03-10 Published:2018-03-07
  • Supported by:
    This work is supported by the Natural Science Foundation of Jiangsu Province (BK20151451).

摘要: 现有自适应软件建模与验证方法较少考虑时间约束,然而,在时间攸关应用领域,自适应软件能否正确运行,不仅要考虑自适应逻辑的正确性,还要考虑自适应软件动态过程的时间特性。为此,首先显式定义了自适应软件的时间特性(监控周期、延迟触发时间、自适应过程截止时间、自适应调节时间和稳定时间等);然后,构造了一种基于时间自动机网络(TAN)的自适应软件动态过程时间特性建模模板;最后,将自适应软件时间特性描述为定时计算树逻辑(TCTL)的形式,并对时间特性进行了形式化分析和验证。结合具体案例验证了该自适应软件时间特性建模和验证方法,结果表明该方法能够显式刻画自适应软件时间特性,降低其形式化建模的难度。

关键词: 自适应软件, 时间特性, 形式化方法, 时间自动机, 模型检验

Abstract: Current modeling and verification approaches for self-adaptive software rarely consider temporal properties. However, in time-critical application domain, the correct operation of self-adaptive software depends on the correctness of self-adaptive logic as well as temporal properties of self-adaptive software dynamic processes. For this end, temporal properties for self-adaptive software were explicitly defined, such as, monitoring period, delay trigger time, deadline of self-adaptive process, self-adaptive adjusting time and self-adaptive steady time. Then, a Timed Automata Network (TAN) based modeling templates for temporal properties of self-adaptive software dynamic processes were constructed. Finally, the temporal properties were formally described with Timed Computation Tree Logic (TCTL), and then were analyzed and verified. Combining with a self-adaptive example, this paper has validated the proposed approach. The results show that the proposed approach can explicitly depict temporal properties of self-adaptive software, and can reduce its formal modeling complexity.

Key words: self-adaptive software, temporal property, formal method, timed automata, model checking

中图分类号: