HPnGs go Non-Linear: Statistical Dependability Evaluation of Battery-Powered Systems
HPnGs go Non-Linear: Statistical Dependability Evaluation of Battery-Powered Systems
复制标题
HPnG 走向非线性：电池供电系统的统计可靠性评估
DOI：
10.1109/mascots.2018.00024
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Anne Remke
中科院分区：
文献类型：
--
作者：
Carina Pilch;Mathis Niehage;Anne Remke
带一般变迁的混合Petri网（HPnGs）为安全关键系统的建模和可靠性评估提供了一种形式化的模型检测方法。HPnG是随机混合自动机的一个受限子类，允许离散、连续和随机变量。以前，离散事件模拟和统计模型检验（SMC）已被用来克服现有分析方法的限制，例如，有限数量的随机变量。此外，在模拟时，连续变量的演化被限制为分段线性轨迹，其中导数在两个事件之间不改变。在这里，我们扩展的建模形式主义，模拟和SMC方法的变量与非线性连续演变。这种扩展的核心思想在于将输入系统转化为所谓的二阶量子化状态系统。动力电池模型的案例研究验证了我们的方法，通过比较的结果，由Matlab得到的。
Hybrid Petri nets with general transitions (HPnGs) provide a formalism for modeling safety-critical systems and evaluating their dependability with means of model checking. HPnGs form a restricted subclass of Stochastic Hybrid Automata and allow discrete, continuous and stochastic variables. Previously, discrete-event simulation and Statistical Model Checking (SMC) have been used to overcome the restrictions of existing analytical approaches, e.g., to a limited number of random variables. Also when simulating, the evolution of continuous variables has been restricted to piecewise-linear trajectories, where derivatives do not change between two events. Here, we extend the modeling formalism, the simulation and SMC approach to variables with a non-linear continuous evolution. The core idea of this extension lies in transforming the input system into a so-called second-order quantized state system. A case study on the Kinetic Battery Model validates our approach by comparing results to those obtained by Matlab.