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

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

作　　者：韩德帅 邢建春 杨启亮 李决龙 

机构地区：[1]陆军工程大学国防工程学院,南京210007 [2]清华大学土木工程系,北京100084 [3]海军海防工程研究中心,北京100841

出　　处：《计算机应用》2018年第3期799-805,共7页journal of Computer Applications

基　　金：江苏省自然科学基金资助项目(BK20151451)~~

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]