第７期 李小勋等：基于ＳＴＡＭＰ的形式化安全性分析 ２８３ ＮＵＳＭＶ、ＳＡＬ等。因为ＮｕＳＭＶ进行建模时从初始值、当前状态 及状态转换的方法三个方面来表示系统的状态转换，所以通过 ＣＴＬ（Ｃｏｍｐｕｔａｔｉｏｎ Ｔｒｅｅ Ｌｏｇｉｃ）语言描述安全性约束。然后通过 模型检测，检测安全性约束是否被破坏 ，实现基于ＳＴＡＭＰ分 析的第５步，使得这种方法相比人工分析更加全面、客观且无 错。因此本文选择了ＮｕＳＭＶ作为形式化分析工具。 ２．１模型检查器ＮｕＳＭＶ ＮｕＳＭＶ进行建模时从初始值、当前状态及状态转换的方法 图１典型的控制结构图 三个方面来表示系统的状态转换。 当有多个控制者进行控制时，多个控制者之间重叠的控制 ＮｕＳＭＶ用关键词ＶＡＲ指示状态变量的定义，这决定了模 和多个控制者之间边界的控制很容易出现问题。这些问题的存 型检查器的状态空间的大小。用关键词ＡＳＳＩＧＮ指示变量的初 在是由于控制者对于控制模型没有充分的理解或控制者之间的 始状态和状态转换的定义，用一系列赋值表达式如ｉｎｉｔ和ｎｅｘｔ 控制模型不一致所导致的。只有控制者充分理解了控制模型中 表示变量的初始状态和状态转换 Ｊ。 各个部分的初始值、当前状态及改变状态的方法时，才能够采取 图３所示为一个ＮｕＳＭＶ模型。 恰当的控制行为。因此基于ＳＴＡＭＰ的安全性分析，应从初始 值、当前状态及改变状态的方法这三方面来分析系统是如何达 到不安全状态的。 １．２分析步骤 基于ＳＴＡＭＰ的安全性分析步骤如图２所示。 ２识 ５确 １识 别系 统级 ３．定 ４识 别导 定这 别系 安全 义控 致危 些异 统危 －．．－－ｏ 相关 —＿ 制结 险的 －－．－Ｉ 常控 险 需求 构图 异常 制发 及约 控制 生的 图３ ＮｕＳＭＶ模型 柬 原因 ２．２ ＣＴＬ语言 图２基于ＳＴＡＭＰ分析步骤 计算树逻辑（ＣＴＬ）是模型检测中用来描述时态逻辑约束的 （１）识别系统危险通过初步危险分析，可以获知系统存 一种常用逻辑。本文只介绍ＣＴＩ＿ 的一个子集，这个子集中包括 在的一些危险。这些危险能够造成人员的伤亡或设备的损坏或 时态算子ＡＧ，ＡＦ，ＡＸ，ＥＧ，ＥＦ，ＥＸｏ可以这样递归地定义ＣＴＬ 环境的污染。 公式子集：一个命题是定义在状态变量上的谓词的布尔组合，一 （２）－／ｇ￣，１系统级安全相关需求及安全性约束在识别出系 个公式或者是一个命题，或者是公式的布尔组合，或者是增加 统的危险之后，应该识别出用于防止这些危险发生的系统级安 ＡＧ，ＡＦ，ＥＧ算子的公式。表１为各个时态算子的解释。 全相关需求及安全性约束。这里所指的安全性约束与一般的功 能需求一样，即要求系统进行某种控制避免系统进入危险状态， 表１ ＣＴＬ时态算子的解释 只不过安全性约束与系统危险有直接关系。 时态算子 解释 （３）定义控制结构图在有了系统需求及安全相关需求与 安全性约束后，可以根据这些需求及安全性约束进行初步的控 ＥＸ ｆ 如果至少一个下一个状态中的ｆ为真 制结构的设计以满足这些需求及安全性约束，并在系统设计不 ＥＦ ｆ 在某些起始于当前状态的路径中，存在某些状态满足ｆ 断细化的过程中，通过分析不断改进控制结构。 ＥＧ ｆ 在某些起始于当前状态的路径中的所有状态满足ｆ （４）识别潜在的异常控制通常来说一个控制者可以产生 ＡＸ ｆ 在每一个下一个状态中ｆ为真 四种类型的异常控制，我们可以根据不同的控制者给出各个控 制者的异常控制行为。 ＡＦ ｆ 在每条起始于当前状态的路径中，存在某些状态满足ｆ ・没有提供需要的控制行为； ＡＧ ｆ 在每条起始于当前状态的路径中，每个状态都满足ｆ ・提供错误的或不安全的控制行为； ・提供的控制行为延迟； 如果系统的每个可达状态都满足公式ｆ，那么说这个系统满 ・提供的控制行为过早结束。 足公式ｆ；否则，模型检测器会尝试找出一个反例。如果公式ＡＧ （５）确定这些异常的控制行为是如何发生的这步是用来 ｆ为假，那么反例就是一条起始于初始状态并终止于不满足ｆ的 分析破坏安全性约束（由（２）得出）的异常控制行为（由（４）得 状态的有限长路径 。 出）是如何发生的。再进行原因分析时可以从初始值、当前状 态、状态转换的方法这三个方面进行分析。分析时既可以采用 ３基于ＳＴＡＭＰ的形式化安全性分析 人工分析方法也可以采用形式化方法。 前两节分别介绍了基于ＳＴｌＶｉＡＰ的安全性分析的原理及步 ２ 形式化分析工具 骤与形式化分析工具ＮｕＳＭＶ。这节将基于ＳＴＡＭＰ的安全性分 析与形式化分析相结合，在ＳＴＡｂｌＰ分析的第５步采用形式化方 进行形式化分析时，可以采用的形式化分析工具有ＳＰＩＮ、 法进行分析。 ２８４ 计算机应用与软件 由执行机构升温。 输入： 约 ２０１２丘 基于ＳＴＡＭＰ形式化安全性分析的步骤如图４所示。 识别 系统 级安 全相 关需 求及 约束 ｌ 识别 系统 危险 定义 控制 识别 导致 危险 束 识 别 ・Ｔｅｍ：由温度传感器感应的温度； ・Ｓｅｔｐｏｉｎｔ：由人进行温度设定。 输出： ・Ｔｅｍ＿结构 图 的异 常控 制 ｌ ｃｏｍｍａｎｄ：温度控制信号。 ４．２安全性分析 （１）识别系统危险 —．Ｉ用ＮｕＳＭＶ建慎Ｉ ｌ执行模型检查Ｉ 大 ＜约柬被破坏？≥＞— 通过 ｌ 给出反例 ｌ 上 经过初步危险分析，温控系统存在如下危险： 模 型 检 测 ・温控系统导致被控制区域温度过高； ・温控系统导致被控制区域温度过低。 这里只对温度过高进行安全性分析。 （２）识别系统安全性需求及约束 查找原因 ＩＩ 工 ｌ更改需求或Ｉｌ 安全性约束ｌ 针对温控系统造成被控制区域的温度过高这种危险，系统 安全性需求及约束如下： ・在有设定值且设定值合理的情况下，当温度高于设定值 图４基于ＳＴＡＭＰ的形式化安全性分析 时，温控系统必须采取降温措施； ３．１约束识别 在ＳＴＡＭＰ分析的前四步，分析出系统的安全性约束与可能 ・在有设定值且设定值不合理时，温控系统要进行异常处 理，即要求设定的温度值不能超过某一值，避免温度过高； ・在没有设定值的情况下，温控系统要按照默认值进行温 度控制，避免温度过高。 （３）定义系统控制结构图 存在的异常控制。在第二步提出的安全性约束是与危险相关的 功能需求，即要求系统执行某种操作以避免系统进入危险状态。 这种安全性约束在模型检测中可作为检测的内容，检测系统在 运行过程中是否破坏安全性约束。在第四步提出的异常控制行 为是与第二步提到的安全性约束相关的控制行为，这些控制行 为都破坏了安全性约束。进行模型检测时检测系统在运行的过 程中是否存在这些异常控制行为。 综上所述，在约束识别过程中应为模型检测提供安全性约 束和破坏这些安全性约束的异常控制行为，以检测这些异常控 制行为是否破坏了与之相应的安全性约束。 根据需求定义的控制结构图如图５所示。（注：Ｔ：温度； ＴＣ：温度控制器；Ｓｅｎｓｏｒ：温度传感器；Ａｃｔｕａｔｏｒ：执行机构；Ｓｅｔ— ｐｏｉｎｔ：设定值） ３．２模型检测 在进行模型检测时，需有模型及要检测的内容。模型指通 图５温控系统控制结构图 由于这个温控系统只是一个简单系统，人只是进行温度的 过系统需求建立起来的模型，即对控制结构图中每个控制单元 进行扩展，用形式化的方法描述各个控制者的初始状态、当前状 态及状态转换方法。要检测的内容指由约束识别得出的安全性 约束，这些安全性约束要用ＣＴＬ语言进行表示，作为模型检查 器检测的内容。有了这两个条件后，就可以通过模型检查器自 设定，并不像典型的控制结构图中的监视者一样起到高级控制 者的作用，所以此处并没有将人在温控系统的控制结构图中 画出。 （４）识别导致危险的异常控制 针对温度过高这种危险，根据ＳＴＡＭＰ给出的四类典型的异 常控制可以给出各个控制者的异常控制。由于篇幅所限只列举 了ＴＣ的异常控制： ・ＴＣ没有发出降温信号； 动地对模型进行遍历，检测是否存在安全性约束被破坏的情况， 如果通过则证明安全性约束没有被破坏。如果安全性约束被破 坏，则给出这些安全性约束是达到被破坏状态的。给出了反例 后，应从各个控制者的初始状态、当前状态及状态转换方法三个 ・ＴＣ发出了错误的降温信号； ・ＴＣ延迟发出降温信号； ・ＴＣ发出的降温信号持续时间过短。 由前四步分析可得模型检测的内容： 方面查找原因，对需求或安全性约束进行更改，不断地反复，直 至所有的安全性约束都通过为止。 ４ 实例 ・安全性约束：在有设定值且设定值合理的情况下，当温 本文对一个温控系统进行了基于ＳＴＡＭＰ的形式化安全性 分析，给出了安全性分析的分析步骤及部分分析结果。 度高于设定值时，温控系统必须采取降温措施； ・异常控制行为：ＴＣ没有发出降温信号。 下面的模型检测过程就是检测这些破坏安全性约束的异常 控制行为是否存在。 （５）用ＮｕＳＭＶ建模 ４．１温控系统简介 温控系统的主要功能是对区域内的温度进行自动控制。当 采集的温度（Ｔｅｍ）高于设定的温度（Ｓｅｔｐｏｉｎｔ）时，温控系统要发 出降温信号（Ａｃｔｉｖｅ），由执行机构进行降温；当温度（Ｔｅｒｎ）低于 此步是在有了系统需求与安全性约束条件下，将需求与安 全性约束用ＮｕＳＭＶ语言进行建模，对最初的控制结构图进行扩 展。扩展后的系统示意图如图６所示。 设定的温度（Ｓｅｔｐｏｉｎｔ）时，温控系统要发出升温信号（Ｄｅａｃｔｉｖｅ）， 第７期 李小勋等：基于ＳＴＡＭＰ的形式化安全性分析 ２８５ 图６扩展后的温控系统控制结构图 图中，Ｔｅｍ：ＴＣ模块的输入温度；Ｔｅｍ—ｓｔａｔｅ：温度状态；Ｃｏｌｄ： 温度低于设定值；Ｈｏｔ：温度高于设定值；Ａｔｓｅｔｐｏｉｎｔ：温度等于设 定值；Ｎｏｎｅ：空；Ｕｎｋｎｏｗｎ：未知状态；Ａｃｔ—ｓｔａｔｅ：执行状态；Ａｃｔｉｖｅ： 降温；Ｄｅａｃｔｉｖｅ：升温；Ｔｅｍ—ｃｏｍｍａｎｄ：ＴＣ模块输出的温控命令； Ｗｏｒｋ：工作状态；Ｉｄｌｅ：空闲状态；Ｔｅｍ—ｉｎ：传感器的输入温度； Ｔｅｒｎ—ｏｕｔ：执行温控操作后的温度。 由于篇幅所限，只对ＴＣ模块进行了详细分析。 图７列出了Ｔｃ模块的模型代码。Ｔｃ模块首先对传感器给 出的Ｔｅｒｎ与Ｓｅｔｐｏｉｎｔ进行比较，得出当前的Ｔｅｍ ｓｔａｔｅ，根据不同 的温度状态决定发送的是升温Ｄｅａｃｔｉｖｅ还是降温Ａｃｔｉｖｅ信号。 最后控制只有在信号发生变化时发送信号，其他隋况下都不发送。 ． 图７ ＴＣ模型代码 （６）模型检测及结果 由于篇幅所限，本文只对温控系统在温度过高时有没有发 送降温信号做检测： ＡＧ（（Ｓｅｔｐｏｉｎｔ＿Ｒｅｃｅｉｖｅ—ｓｔａｔｅ＝Ｈａｖｅ—ｒｅｃｅｉｖｅｄ＆Ｔｅｒｎ—Ｒｅｃｅｉｖｅ—ｓｔａｔｅ＝ Ｈａｖｅｒｅｃｅｉｖｅｄ＆ＴＣ．Ｔｅｒｎｓｔａｔｅ＝Ｈｏｔ） 一＞！ＥＦ ＴＣ．Ｔｅｍ—ｃｏｍｍａｎｄ：Ｄｅａｃｔｉｖｅ） 即：在起始条件下，当收到（Ｈａｖｅ—ｒｅｃｅｉｖｅｄ）Ｔｅｎｒ与Ｓｅｔｐｏｉｎｔ 值时，且Ｔｅｒｎ—ｓｔａｔｅ为热（Ｈｏｔ）的情况下，不存在温控命令（Ｔｅｒｎ— ｃｏｍｍａｎｄ）Ｄｅａｃｔｉｖｅ。进行模型检测的结果显示，这种假设是错 的，即存在一条反例证明在起始条件下，当收到温度值与设定值 且温度状态为Ｈｏｔ的情况下，存在升温命令。模型检查器给出 的反例如下所示： 第一步： Ｔｅｍｒｅｃｅｉｖｅ—ｓｔａｔｅ＝Ｎｏｎｅ ＿Ｓｅｔｐｏｉｎｔｒｅｃｅｉｖｅ——ｓｔａｔｅ：Ｎｏｎｅ ＴＣ．Ｔｅｍｓｔａｔｅ＝Ｎｏｎｅ —ＴＣ．Ｔｅｒｎ—ｃｏｍｍａｎｄ＝Ｎｏｎｅ ＴＣ．Ｃｏｍｍａｎｄ＿ｌｆａｇ Ｎｏａｃｔ Ｔｅｒｎ＝２５ Ｓｅｔｐｏｉｎｔ＝２５ 第二步： Ｔｅｍｒｅｃｅｉｖｅ ｓｔａｔｅ＝Ｈａｖｅ＿—ｒｅｃｅｉｖｅｄ Ｓｅｔｐｏｉｎｔｒｅｃｅｉｖｅｓｔａｔｅ Ｈａｖｅ———ｒｅｃｅｉｖｅｄ Ｔｅｍ＝２６ 第三步： ＴＣ．Ｔｅｍｓｔａｔｅ＝Ｈｏｔ —Ｔｅｍ＝０ 第四步： ＴＣ．Ｔｅｒｎ—ｓｔａｔｅ＝Ｃｏｌｄ ＴＣ．Ｔｅｒｎ—ｃｏｍｍａｎｄ＝Ａｃｔｉｖｅ ＴＣ．Ｃｏｍｍａｎｄ＿ｆｌａｇ＝Ｓｅｎｄ Ｔｅｍ＝２６ 第五步： Ｔｅｍｒｅｃｅｉｖｅｓｔａｔｅ：Ｈａｖｅｒｅｃｅｉｖｅｄ ———Ｓｅｔｐｏｉｎｔｒｅｃｅｉｖｅ——ｓｔａｔｅ＝Ｈａｖｅｒｅｃｅｉｖｅｄ ＴＣ．Ｔｅｍｓｔａｔｅ＝Ｈｏｔ ＴＣ．Ｔｅｒｎ＿ｃｏｍｍａｎｄ＝Ｄｅａｃｔｉｖｅ Ｔｅｒｎ＝０ 由上面的第五步可知，存在温度状态为Ｈｏｔ却升温的情况，这 种情况的存在会造成被控制区域温度过高的危险。通过上边的模 型检测结果可以看出，造成这种情况的原因是在第三步中Ｔｅｍ— ｃｏｍｍａｎｄ没有及时发送，导致第四、五步发送的Ｔｅｒｎ＿ｃｏｍｍａｎｄ的命 令都有延迟。因此需要对安全性需求或安全性约束进行相应的更 改以保证每次发送的Ｔｅｍ＿ｃｏｍｍａｎｄ与Ｔｅｍ＿ｓｔａｔｅ一致。 ５ 结语 本文将基于ＳＴＡＭＰ的安全性分析与形式化的方法相结合， 给出了基于ＳＴＡＭＰ的形式化安全性分析方法。采用这种方法 不是仅强调失效引起的危险，因此能够更加有效地对系统进行 安全性分析，提高系统的安全性。结合形式化分析，可以减少由 于分析者经验不足引起的分析不充分或分析结果太主观等问 题。本文只是初步地对基于ＳＴＡＭＰ的形式化安全性分析进行 研究，今后将对其做更进一步的研究。 参考文献 ［１］Ｌｅｖｅｓｏｎ Ｎ Ｇ．Ａ Ｎｅｗ Ａｃｃｉｄｅｎｔ Ｍｏｄｅｌ ｆｏｒ Ｅｎｇｉｎｅｅｒｉｎｇ Ｓａｆｅｒ Ｓｙｓｔｅｍｓ ［Ｊ］．Ｓａｆｅｔｙ Ｓｃｉｅｎｃｅ，Ｅｌｓｅｖｉｅｒ，Ａｐｒｉｌ ２００４，４２（４）． ［２］Ｔｒｉｈｂｌｅ Ａ Ｃ，Ｍｉｌｌｅｒ Ｓ Ｐ，Ｌｅｍｐｉａ Ｄ Ｌ．Ｓｏｆｔｗａｒｅ Ｓａｆｅｔｙ Ａｎａｌｙｓｉｓ ｏｆ ａ ＦｌＪ ｇｈｔ Ｇｕｉｄａｎｃｅ Ｓｙｓｔｅｍ［Ｃ］／／Ｄｉｉｇｔａｌ Ａｖｉｏｎｉｃｓ Ｓｙｓｔｅｍｓ Ｃｏｎｆｅｒｅｎｃｅ， ２００２．Ｐｒｏｃｅｅｄｉｎｇｓ．Ｔｈｅ ２１ｓｔ ２００２，２：１３Ｃ１一ｌ－１３Ｃ１—１０． ［３ ｊ Ｍｅｅｎａｋｓｈｉ Ｂ，Ｂａｒｍａｎ Ｋ Ｄ，ＢａｂｕＬ Ｇ，ｅｔ ａ１．Ｆｏｒｍａｌ Ｓａｆｅｔｙ Ａｎａｌｙｓｉｓ ｏｆ Ｍｏｄｅ Ｔｒｎａｓｉｔｉｏｎｓ ｉｎ Ａｉｒｃｒｆａｔ Ｆｌｉｇｈ【Ｃｏｎｔｒｏｌ Ｓｙｓｔｅｍ［Ｃ］／／Ｄｉｉｇｔａｌ Ａｖｉｏｎ— ｉｃｓ Ｓｙｓｔｅｍｓ Ｃｏｎｆｅｒｅｎｃｅ，２００７．ＤＡＳＣ ０７．ＩＥＥＥ／ＡＩＡＡ ２６ ｔｈ． ［４］黄光华，段川，蒋凡．基于Ｍｏｄｅｌ Ｃｈｅｃｋｉｎｇ的系统脆弱性分析［Ｊ］． 计算机工程，２００５，３１（４）．
