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.
翻译:以软件组件与环境的封闭互动为特征的系统行为不可避免地受到干扰和不确定因素的影响。我们在本文件中提议了对这些系统行为要求的规格和核查的一般框架。我们引入了 " 演变时逻辑 " (EvTL),这是STL的随机扩展,使我们能够具体说明描述系统瞬时行为概率分布的特性,并将不确定性包含在规格中。我们为 EvTL 配备了坚固的语义学,并证明它对于进化指标所引发的语义学来说是合理和完整的,即表明一个系统如何很好地完成另一个系统的任务。最后,我们为EvTL 规格开发了一个统计模型核对算法。作为我们框架应用的一个实例,我们考虑一个三罐实验室实验。