论文标题
EVTL：用于网络物理系统瞬时分析的时间逻辑
EvTL: A Temporal Logic for the Transient Analysis of Cyber-Physical Systems
论文作者
论文摘要
以软件组件与环境的封闭相互作用为特征的系统行为不可避免地会受到扰动和不确定性的影响。在本文中，我们提出了一个通用框架，以规范和验证这些系统行为的要求。我们介绍了Evolution Perimal Logic（EVTL），这是STL的随机扩展，使我们能够指定描述系统瞬态行为的概率分布的属性，并在规范中包括不确定性的存在。我们为EVTL配备了稳健性的语义，并且与进化指标引起的语义有关，即表达系统如何满足其任务相对于另一个人的任务。最后，我们为EVTL规范开发了统计模型检查算法。作为应用框架的一个例子，我们考虑了一个三坦克实验室实验。
The behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to perturbations and uncertainties. In this paper we propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Evolution Temporal Logic (EvTL), a stochastic extension of STL allowing us to specify properties of the probability distributions describing the transient behaviour of systems, and to include the presence of uncertainties in the specification. We equip EvTL with a robustness semantics and we prove it sound and complete with respect to the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we develop a statistical model checking algorithm for EvTL specifications. As an example of an application of our framework, we consider a three-tanks laboratory experiment.
