交互式系统建模的模型组合

# 交互式系统建模的模型组合 在交互式系统建模中，我们需要将功能模型和交互模型进行有效组合，以确保系统既满足功能需求，又具备良好的交互性。下面将详细介绍相关的模型和方法，并通过核电站案例进行说明。 ## 1. 展示模型关系（PMR） 展示模型关系（PMR）为展示模型中的S - 行为赋予意义，就像PIM为I - 行为赋予意义一样。S - 行为代表系统的功能行为，在形式化规范中进行了定义。PMR是从展示模型中的所有S - 行为到规范中操作的多对一关系，这反映了用户通常可以通过多种方式从用户界面执行任务，因此可能有多个不同的S - 行为与规范中的单个操作相关。 例如，对于展示模型元组中的行为标签S_IncWaterPressure1，我们可以从PMR中确定它在Z规范中所代表的操作名称： ```plaintext S_IncWaterPressure1 ↦ IncreaseWaterPressure ``` 这表明在形式化规范中有一个名为‘IncreaseWaterPressure’的操作，该操作规定了此操作对系统的影响，从而为这个行为标签赋予了意义。 ## 2. 规范 系统的形式化规范提供了系统状态以及操作对该状态允许更改的明确描述。有许多不同的形式化语言可用于此类规范，如VDM、Z、B、Event - B和Object - Z等。我们采用基于集合论和一阶谓词逻辑的Z规范语言。 在Z中，我们通常根据对系统的观察来描述被建模的系统，然后操作描述展示了观察到的值如何变化。操作由前置条件和后置条件进行约束，前置条件规定了操作允许发生的情况，后置条件定义了操作发生时哪些观察值会改变，哪些不会改变，以及任何输出值。 以核电站为例，规范涉及与反应堆压力和水位、冷凝器压力和水位、功率输出、泵的速度以及阀门状态等项目相关的观察。Z规范可以与定理证明器一起使用，以证明系统整个状态空间的属性，也可以与模型检查器一起使用，检查约束状态空间中的安全条件等。 ## 3. μCharts 除了Z规范，我们还使用可视化语言μCharts来建模反应式系统。PIM也可以表示为μcharts，它比简单的PIM具有更多优势，例如能够通过反馈机制在不同图表中组合特定的行为集，并将复杂图表嵌入简单状态以“隐藏”复杂性。 μCharts基于Harel Statecharts开发，语法比Statecharts更简单，并且具有形式化语义。μCharts和Statecharts在转换的同步性、步骤语义和转换标签的性质方面存在差异。μcharts中的转换标签形式为guard∕action，其中guard是一个谓词，如果为真则触发转换并执行相应的action。例如，如果guard是一个信号s，那么当前步骤中存在s会使guard为真。guard的评估和action的执行在同一单步中瞬间完成。 μCharts语言包含多个细化理论，这也为PIM提供了细化理论。其中，μCharts的跟踪细化理论特别有用，它可以抽象为基于契约效用的更轻量级的接口细化理论。μCharts的语义用Z表示，并且可以通过算法和工具将μchart直接转换为Z规范，进而将PIM转换为Z规范。 ## 4. 模型组合 功能模型（规范）和交互模型（展示模型和PIM）已经通过PMR进行了耦合，这使我们得到一个将传统的Z规范用于功能描述与更具视觉吸引力的图表用于交互描述相结合的模型。 我们还可以将这些模型组合成一个全Z的单一模型，用于整个系统。这样可以创建一个交互式系统所有部分（交互性和底层功能）的单一模型，用于证明与功能约束、接口约束或两者相关的系统安全属性，也可以作为通过Z的细化理论最终实现系统的基础。 我们通过使用μCharts的Z语义并将PMR表示为Z关系来构建这个单一模型。然后将其与系统功能的形式化规范相结合，使代表PIM的转换用于约束操作的可用性。例如，如果展示模型中的某个S - 行为仅在用户界面的一个状态下可用，那么在新的组合Z规范中，这将表示为相关操作的前置条件。 ## 5. 核电站案例研究 ### 5.1 Z规范建模 根据案例研究中核电站功能的概述和一些假设，我们可以生成所需