使用ISO标准Z和CADiZ证明Stateflow模型的属性

### 使用ISO标准Z和CADiZ证明Stateflow模型的属性 #### 1. 离散输出假设 离散输出假设（DiscreteOutputs Anns）的定义如下： ```plaintext DiscreteOutputs Anns == ⟨| next == [Sig Statechart ′ ; Sig Statechart | (¬ DELAY 2?′ ⇒¬ START?) ∧ (DELAY 2?′ ∧¬ START?′ ∧ NG?′ > BLexicon.NGmax1fromstarter ⇒ NG? ≤NG?′) ∧ (DELAY 2?′ ∧¬ START?′ ∧ NG?′ ≤BLexicon.NGmax1fromstarter ⇒ NG? < 59) ∧ (START?′ ∧ NG?′ < BLexicon.NGmax2fromstarter ⇒ NG? ≥NG?′) ∧ (START?′ ∧ NG?′ ≥BLexicon.NGmax2fromstarter ⇒ NG? ≥10) ∧ (DELAY 2?′ ∧NG?′ < 15 ⇒NG? < 59) ∧ (DELAY 2?′ ⇒DELAY 2?)] [Other assumptions elided...] |⟩ ``` 这些关于根状态的下一个假设具有两个重要原因： - **表达模型对环境的假设**：这些假设并非用户预先编写，而是PFS分析的结果。用户可以根据需要向父状态添加下一个假设，以确保健康性条件有效，最终形成对根状态的这些假设。 - **关联输入的预期值和先前值**：这些假设将输入的预期下一个值与输入的先前（带撇号）值相关联，从而可以约束输入的变化率和范围。这里使用撇号表示先前值，与通常的Z约定相反。 #### 2. 健康性条件 健康性条件用于检查Stateflow模型的各种属性，以下是一些常见的健康性条件及其形式化表示： - **下一个假设是否成立（Next Assumptions Established）**：对于任何子状态，其下一个假设是否由其配置的最后假设和其父状态的下一个假设所确立？ ```plaintext Next InitialState == ⊢? ∀Sig Statechart ′ ; Sig Statechart | DiscreteOutputs Anns.last ′ ∧InitialState Anns.last ′ ∧ DiscreteOutputs Anns.next • InitialState Anns.next ``` - **最后假设是否成立（Last Assumptions Established）**：对于状态之间的任何转换，其目标配置的最后假设是否由其触发条件、源状态的下一个假设和源配置的最后假设所确立？ ```plaintext Last EngineRunning InitialState == ⊢? ∀Sig Statechart ′ ; Sig Statechart | DiscreteOutputs Anns.last ′ ∧InitialState Anns.last ′ ∧ InitialState Anns.next ∧ InitialState Anns.trigger EngineRunning • DiscreteOutputs Anns.last ∧NormalOperation Anns.last ∧ StartSwitchOffAnns.last ∧EngineRunning Anns.last ``` - **最后假设是否保留（Last Assumptions Preserved）**：对于任何基本状态，其配置的最后假设是否由其下一个假设和状态保留条件所保留？ ```plaintext Last InitialState SPC == ⊢? ∀Sig Statechart ′ ; Sig Statechart | DiscreteOutputs Anns.last ′ ∧InitialState Anns.last ′ ∧ InitialState Anns.next ∧InitialState Anns.spc • DiscreteOutput Anns.last ∧InitialState Anns.last ``` - **初始