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

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

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

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.