一种基于微分代数时序动态逻辑的CPS属性验证方法

摘要

本发明提出了一种基于微分代数时序动态逻辑的CPS属性验证方法，用于对CPS进行系统建模、属性规约和属性验证。本发明涉及到的关键操作包括：(1)在对CPS详细分析的基础上，使用微分代数程序对CPS进行系统建模，得到系统的操作模型；(2)使用DATL对要验证的CPS属性进行规约，得到DATL公式，此规约过程考虑了CPS的时序行为；(3)使用DATL中的相继式演算对前面得到的DATL公式进行验证，整个演算过程是通过不断地使用DATL规则来进行推理，最后得出DATL公式成立，也就是CPS属性满足。

主权项

一种基于微分代数时序动态逻辑的CPS属性验证方法，其特征在于，用微分代数时序动态逻辑DATL对信息物理融合系统CPS进行系统建模、属性规约和属性验证，包括如下步骤：步骤1)分析待验证的CPS，用微分代数程序对其建模，得到系统的操作模型α；步骤2)分析要验证的CPS属性，用DATL对其规约，规约成DATL公式的形式；该形式是形如ψ→[α]□φ，其中：ψ表示前提条件；[α]是操作模型α的模态，表示对于α的所有执行轨迹的最终状态；□是时序操作符，表示任意时刻或任意状态；[α]□表示对于α的所有执行轨迹的任意一个中间状态；φ表示要满足的某种约束；整个式子ψ→[α]□φ表示如果初始时刻ψ成立，那么对于α的所有执行轨迹上的任意一个中间状态，约束φ都是成立的；步骤3)使用DATL的相继式演算，结合DATL中的演算规则，对步骤2)中得到的DATL公式ψ→[α]□φ进行推理验证，推理过程是：每次使用一个演算规则，推导出一个公式，然后，再次使用一个演算规则推导出另一个公式，如此进行；步骤4)如果步骤3)中的推理最后推导出公理ax，则推理过程结束，要验证的属性满足，验证完毕；步骤5)如果步骤3)中的推理最后推导不出公理ax，那么本基于微分代数时序动态逻辑的CPS属性验证方法不能得出属性是否满足的结论，步骤6)结束验证；所述步骤1)中，微分代数程序定义如下：a、微分代数程序DAP是如下递归定义的最小集合：1)如果J是DJ约束，那么J是DAP；2)如果D是DA约束，那么D是DAP；3)如果α,β∈DAP，那么(α∪β)∈DAP；4)如果α,β∈DAP，那么(α；β)∈DAP；5)如果α∈DAP，那么(α*)∈DAP；b、DJ约束是如下递归定义的最小集合：1)DJ约束的原子公式是DJ约束；2)若A是DJ约束,则()也是DJ约束；3)若A,B是DJ约束,则(A∧B),(A∨B),(A→B),()也是DJ约束；4)若A是DJ约束,则也是DJ约束；5)只有有限次地应用1)‑4)构成的符号串才是DJ约束；6)规定DJ约束中的赋值语句x:＝θ不会出现在的辖域内；c、DJ约束的原子公式是如下定义的集合：1)赋值语句x:＝θ是DJ约束的原子公式,其中x＝(x₁,x₂,…,x_n),x₁,x₂,…,x_n分别是个体变项符号，θ＝(θ₁,θ₂,…,θ_n)，θ₁,θ₂,…,θ_n分别是DJ约束的项；2)设R(x₁,x₂,…,x_n)是DJ约束的n元谓词符号，t₁,t₂,…,t_n是DJ约束的n个项，则称R(t₁,t₂,…,t_n)是DJ约束的原子公式；d、DJ约束的项是如下递归定义的最小集合：1)个体常项符号、个体变项符号是DJ约束的项；2)若是n元函数符号，t₁,t₂,…,t_n是n个DJ约束的项，则是DJ约束的项；3)所有的DJ约束的项都是有限次使用1),2)得到的；e、DA约束的定义：DA约束是定义在∑∪∑′上的一阶逻辑公式，其中∑为状态变量、函数和谓词关系的集合，∑′为∑中状态变量x的导数x′的集合，且∑′中的符号x′不能出现在的辖域内，DA约束中的状态变量x有可能改变当且仅当DA约束中出现x′。