Statistical Verification of Hyperproperties for Cyber-Physical Systems
Statistical Verification of Hyperproperties for Cyber-Physical Systems
复制标题
DOI：
10.1145/3358232
复制
发表时间：
2019-06
期刊：
影响因子：
--
通讯作者：
Yu Wang;Mojtaba Zarei;Borzoo Bonakdarpour;Miroslav Pajic
中科院分区：
文献类型：
--
作者：
Yu Wang;Mojtaba Zarei;Borzoo Bonakdarpour;Miroslav Pajic
信息物理系统（CPS）的许多重要属性都是基于连续时间内多个执行之间的关系来定义的。示例包括概率公平性和对建模误差的敏感性（即，参数变化）。这些要求只能由hyperproperties指定。在这篇文章中，我们专注于验证CPS的概率超性质。为了涵盖广泛的建模形式主义，我们首先提出了一个通用模型的概率不确定系统（PUSs），统一了通常研究的CPS模型，如连续时间马尔可夫链（CTMCs）和概率参数化混合I/O自动机（P2 HIOA）。为了正式指定hyperproperties，我们提出了一个新的时序逻辑，超概率信号时序逻辑（HyperPSTL），作为一个超和概率版本的传统信号时序逻辑（STL）。考虑到现实世界中的系统，可以被捕获为PUSs的复杂性，我们采用了统计模型检查（SMC）的方法进行验证。我们开发了一种新的SMC技术的基础上直接计算的显着性水平的统计断言的HyperPSTL规范，它不需要先验知识的无差异保证金。然后，我们介绍了SMC算法的HyperPSTL规范的联合概率分布的多条路径，以及规范与嵌套的概率算子量化不同的路径，这不能处理现有的SMC算法。最后，我们证明了我们的SMC算法的有效性CPS基准具有不同程度的复杂性，包括丰田动力总成控制系统。
Many important properties of cyber-physical systems (CPS) are defined upon the relationship between multiple executions simultaneously in continuous time. Examples include probabilistic fairness and sensitivity to modeling errors (i.e., parameters changes) for real-valued signals. These requirements can only be specified by hyperproperties. In this article, we focus on verifying probabilistic hyperproperties for CPS. To cover a wide range of modeling formalisms, we first propose a general model of probabilistic uncertain systems (PUSs) that unify commonly studied CPS models such as continuous-time Markov chains (CTMCs) and probabilistically parametrized Hybrid I/O Automata (P2HIOA). To formally specify hyperproperties, we propose a new temporal logic, hyper probabilistic signal temporal logic (HyperPSTL) that serves as a hyper and probabilistic version of the conventional signal temporal logic (STL). Considering the complexity of real-world systems that can be captured as PUSs, we adopt a statistical model checking (SMC) approach for their verification. We develop a new SMC technique based on the direct computation of significance levels of statistical assertions for HyperPSTL specifications, which requires no a priori knowledge on the indifference margin. Then, we introduce SMC algorithms for HyperPSTL specifications on the joint probabilistic distribution of multiple paths, as well as specifications with nested probabilistic operators quantifying different paths, which cannot be handled by existing SMC algorithms. Finally, we show the effectiveness of our SMC algorithms on CPS benchmarks with varying levels of complexity, including the Toyota Powertrain Control System.