有限状态机在导弹发射安全性分析中的应用*

刘旭，刘艳，王冬，韩颖超，张为雯

(北京电子工程总体研究所，北京 100854)

0 引言

空空导弹发射过程表现出复杂的逻辑关联，其飞控系统需要监测和控制相关弹上设备状态，同时输入输出变量之间存在复杂的逻辑关联，对其逻辑特性进行安全性分析，即验证系统的状态迁移序列是否按照合理有效的顺序执行，是开展机弹安全性分析过程中的一大重点。

有限状态机模型提供了描述和控制功能逻辑非常强大的方法，复杂逻辑往往可以通过图表化形式表述，规则简单，它通过对状态图、流程图的创建，对事件驱动系统进行建模分析[1-6]。

国外Simfia软件可将状态机模型自动转化为相应的AltaRica形式化模型，再利用AltaRica模型的特征，自动仿真推演某个事件触发后可能引发的故障行为。然而，形式化方法采用有严格定义的语义及符号对系统的各部分建模，按照规范对研究对象进行严格的安全性验证，可增强对系统细节的理解，尽早发现系统规范中存在模糊性、二义性的地方，但形式化方法不利于理解，且建模过程复杂[7]。

为此，本文以有限状态机的完备功能逻辑提取特性为基础，研究提出状态迁移建模分析方法，有效兼顾了描述系统功能的状态机模型涉及到的初始状态、有效状态、状态转移条件等各分析要素[8-9]，表述形式直观易懂，较之传统的有限状态机理论具有更大的工程可操作性，极大地降低了形式化建模语言带来的分析难度。

1 基于有限状态机的状态迁移建模分析方法

1.1 有限状态机基本原理

有限状态机作为一种具有离散输入和输出系统的数学模型，是指系统内有有限个内部状态，在某些事件发生时，系统从一个状态转换到另一个状态，又称为事件驱动系统。

有限状态机的要素包括：状态集(若干个状态)；状态之间的转换关系(全体有向弧表示这种关系)；输入集(状态之间的转换所需输入构成)；开始和结束状态。利用形式化语言定义，可将有限状态机定义为6元组[10]：

M=(Σ,O,S,S0,Δ,Λ)，

(1)

式中：Σ为输入集合；O为输出集合；S为M中有限状态的集合；S0为初始状态的集合；Δ(s,x)为状态转移函数(Δ：S×Σ→S)；Λ(s,x)为输出函数(Λ：S×Σ→O)；集合Σ，O，S定义为非空集合；Δ和Λ是多输出的布尔函数。

M中的转移关系TM:S×Σ×S→{0,1}，它描述了所有由一段弧连接的状态对(x,y)∈S×S，将弧标记为ω，ω∈Σ，Tm定义为

(2)

式中:x1,…,xm为当前状态变量；ω1,…,ωm为原始的输入变量；y1，…，ym为有限状态机的下个状态变量。形式化方法实质是采用数学理论描述复杂逻辑系统采用严格定义语言完成系统各部分的建模，具有严谨的数学基础。随着导弹发射控制涉及的硬件和软件规模的扩大，系统复杂度也大大提高，需借助于一套复杂的状态表达式和路径表达式来操作时钟、控制等各类变量及其计算模型，基于形式化分析与验证越发困难[11-15]。

1.2 状态迁移建模要素及方法

本文基于有限状态机原理提出了具有工程可操作性的状态迁移模型，半定性地描述系统工作状态之间的迁移条件关系，以及工作状态与相应功能和接口之间的关联关系及约束关系。这种支持图形界面的定性方法相对于形式化建模分析语言更易于理解。

状态迁移模型的图形化建模元素包括：

(1) 工作状态：系统运行过程中所有可能的工作状态或模式。

(2) 迁移条件：某个工作状态向其他工作状态发生迁移的条件关系。迁移条件通常可由系统外部输入输出接口、功能等其他需求模型元素进行描述。需要说明的是，一个工作状态既有迁入条件，又有迁出条件。

(3) 初始状态：系统运行起始点，只用于状态迁移图的起始描述，不具备实际意义。

(4) 结束状态：系统运行终点，只用于状态迁移图的终止描述，不具备实际意义。

(5) 注释：在图形化建模过程中，可利用“注释”对话框来注明每项建模元素的备注信息(例如约束信息、展开描述等)。

状态迁移模型的图形化建模元素图例如表1所示。

表1 状态迁移模型建模元素Table 1 Composition of state migration model

状态迁移建模分析流程如图1所示。

状态迁移建模是一个重复的过程，在存在并行执行的状态下，有的迁移流程可能会缺少初始状态。需要把最初定义的初始状态细化成各个转移流程中的初始状态，从而引出新的状态。因此，在进行后一步工作时，要不断地返回上一步进行修改或完善，从而使建模更加准确和清晰。

2 空空导弹发射安全性分析

2.1 确定发射状态迁移模型

针对空空导弹典型作战过程中不同阶段状态迁移进行建模，将导弹发射生存周期状态划分成加电、自检、对准、准备、发射、自主飞行、故障和应急投弃状态，以导弹状态、载机参数条件、飞行员操作作为状态转换条件，建立的空空导弹典型发射状态迁移图形化建模如图2所示。图中各个状态的描述见表2。

2.2 分析发射状态转移关系模型

基于导弹发射控制状态机模型，识别状态迁移关系。由此建立的源状态至目的状态的迁移关系见表3。

2.3 发射异常迁移条件识别

针对上一步骤识别的每个状态迁移关系，按照表4的要求，依次进行当前迁移条件分析及异常状态迁移条件分析。

图1 状态迁移建模分析流程Fig.1 Flow chart of state migration modeling

图2 空空导弹发射过程状态迁移图Fig.2 State migration diagram of air-to-air missile launching

以应急投弃为目的状态的所有状态迁移(1→9，2→9，3→9，4→9，5→9，6→9，8→9)为例填写上表，则：

(1) 状态迁移：填写所分析的状态迁移，即“1→9,2→9,3→9,4→9,5→9,6→9,8→9”。

(2) 当前迁移条件：当飞行员进行按压应急投弃开关的操作，触发相应迁移。因此，在“飞行员操作”一栏填写“按压应急投弃开关”。

(3) 异常迁移条件：可从以下方面开展分析当前迁移条件的不合理因素，包括。

1) 条件充分性：如各状态的进入条件、退出条件、约束条件不够完整；等等。

2) 条件协调性：如各状态的进入条件和退出条件不一致、状态退出条件永远无法满足等。

3) 多状态迁移：如当前状态下，向多个状态的转移条件同时成立等。

4) 潜通路：如不可相互迁移的状态间发生了状态迁移。

5) 状态冲突：如互斥状态迁移同时出现等。

因此，从条件充分性方面分析出“进入应急投放状态时，缺少飞机轮载信号的判断”这一异常状态迁移条件。从潜通路方面分析出“响应误操作按压的投弃致使意外抛弃导弹”这一异常状态迁移条件。

表3 状态迁移关系Table 3 Migrating workflow

表4 异常状态迁移分析Table 4 Analysis of abnormal precondition of state change

2.4 发射异常迁移条件控制

从异常迁移条件出发进行系统安全性分析，分析点包括在所有对应的功能中，关联度高的若干功能同时失效的安全性问题；或者从路径角度分析，如果路径迁移设计得不够周到所存在的安全性问题，最终基于以上2方面的结果得出潜在的导致空空导弹发射危险的不安全迁移条件及其控制措施，见表5。

表5 异常迁移条件控制措施示例Table 5 Example of prevention and control on abnormal precondition of state change

3 结束语

本文将有限状态机理论应用于复杂装备安全性建模分析中，通过对状态机理论模型中涉及到状态和转移部分进行简化，建立了由初始状态、状态和转移关系所构成的状态迁移模型。以“状态图”这种半形式化模型与“分析表格”相结合的方式，可以清晰、简洁地反映出复杂系统动态逻辑关系，为明确事故的动态变化过程和制定控制措施提供了依据，弥补了基于形式化建模语言的有限状态机模型抽象、不易理解而难以在工程上推广应用的不足。