Cyber-physical systems are systems that exhibit both discrete computational and continuous physical behavior. They are often subject to different kinds of uncertainty, ranging from sensor noise over random component failures to inconfidences induced by sample-based statistical learning. Quantitative formal methods have proven to be especially useful for assessing the impact of uncertainty on the system evolution over time. However, they lack compositionality. Existing methods for compositional design and verification, such as contracts, traditionally abstract from or (over-)approximate probability distributions, and resort to purely qualitative safety assessments in worst-case scenarios. This paper proposes a first step towards the integration of probabilistic methods into contract-based verification schemes to enable compositional reasoning over uncertain system behavior. We discuss different sources of uncertainties, as well as the necessity of probabilistic contracts for cyber-physical systems. Our key idea for integrating probabilities into contracts is the identification of safe yet precise approximations for sets of distributions, for which we use subdistributions. With that, we hope to reconcile probabilistic with set-based reasoning.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Towards Probabilistic Contracts for Intelligent Cyber-Physical Systems

  • Pauline Blohm,
  • Martin Fränzle,
  • Paula Herber,
  • Paul Kröger,
  • Anne Remke

摘要

Cyber-physical systems are systems that exhibit both discrete computational and continuous physical behavior. They are often subject to different kinds of uncertainty, ranging from sensor noise over random component failures to inconfidences induced by sample-based statistical learning. Quantitative formal methods have proven to be especially useful for assessing the impact of uncertainty on the system evolution over time. However, they lack compositionality. Existing methods for compositional design and verification, such as contracts, traditionally abstract from or (over-)approximate probability distributions, and resort to purely qualitative safety assessments in worst-case scenarios. This paper proposes a first step towards the integration of probabilistic methods into contract-based verification schemes to enable compositional reasoning over uncertain system behavior. We discuss different sources of uncertainties, as well as the necessity of probabilistic contracts for cyber-physical systems. Our key idea for integrating probabilities into contracts is the identification of safe yet precise approximations for sets of distributions, for which we use subdistributions. With that, we hope to reconcile probabilistic with set-based reasoning.