题目：STAMP语境下安全性分析建模语言与执行技术研究

在系统理论事故模型（STAMP）中，事故的根本原因是由于系统运行过程中没有保证应该满足的安全性约束。基于STAMP的安全性分析方法（STPA）的核心工作就是识别系统中的控制缺陷，对于软件密集的计算机控制系统，安全性约束的破坏大多数是由软件需求中引入了控制缺陷，导致系统运行过程中，控制器或操作者发出错误的控制行为，违反相应的安全性约束，使系统处于危险状态甚至导致事故。传统上，对于软件需求缺陷的识别工作主要靠专家评审或者借助安全性分析方法进行验证的方式进行，容易受人员素质的影响，缺乏效率和有效性。因此，本文根据软件需求的特点，提出构建形式化有限状态机模型，通过模拟系统运行行为的方式识别软件需求中的控制缺陷的研究思路。文章首先使用过程控制模型来描述计算机过程控制系统，研究过程控制模型中不同元素在系统运行过程中的作用，根据计算机控制控制器软件需求的特点，提出了一种较为合理的形式化的有限状态机模型，并试图通过对该模型进行分析识别出需求中的控制缺陷。为完成这一目标，本文从需求的有限状态机的角度总结和提出了一些与安全性有关的需求约束，并通过一个示例演示了建立需求有限状态机模型并识别需求缺陷的原理。在利用需求有限状态机进行缺陷识别过程中，首先需要利用合适的建模语言对需求状态机进行建模，本文选取可读性较高、容易书写的形式化语言SpecTRM-RL并进行改进，作为需求有限状态机的建模语言，构建需求状态机模型；通过对SpecTRM-RL语言、NuSMV程序语言和时态逻辑理论进行深入研究，给出了将SpecTRM-RL模型转化为NuSMV程序的规则，借助NuSMV模型检测工具执行需求状态机的缺陷识别。综上所述，就形成了一个针对需求的有限状态机进行形式化建模和执行缺陷识别的完整方案。文章最后针对一个实例系统，采用本文研究取得的针对需求的形式化建模和执行缺陷识别，验证了论文研究成果的有效性。