摘要：注2:在GB/T 20438.2-2017的表B.1、表B.2和表B.6以及在GB/T 20438.3-2017的表A.1、表A.2、表A.4、表B.7,表C,1,表C.2、表C.4和表C.17中引用了本技术/措施。

B.2.3 半形式化方法

注1:在GB/T 20438.3-2017的表B.7中采用其他半形式化的软件相关技术扩展了这个附录B的列表。列表如下:

——逻辑/功能块图:在GB/T 15969.3中描述；

——顺序图:在GB/T 15969.3中描述;

——数据流图:见C.2.2;

——有限状态机/状态转换图:见B.2.3.2;

——时间佩特里(Petri)网:见B.2.3.3;

——实体-关系-属性数据模型:见找2.4.4;

——消息序列图:见C.2.14;

——判定/真值表:见C.6.1。

目的:为了清楚地和一致地表达一份规范的各部分,以便能检查出某些错误、遗漏和不正确的行为。

注2:在GB/T 20438.2-2017的表B.1、表B.2和表B.6以及在GB/T 20438.3-2017的表A.1、表A.2、表A.4、表B.7,表C,1,表C.2、表C.4和表C.17中引用了本技术/措施。

B.2.3.1 概述

目的:为了证明设计满足它的规范。

描述:半形式化方法为在开发一个系统的某个阶段编制该系统的描述(即规范、设计或者编码)提供了一种方法。在某些情况下,可用机器分析该描述,或者为了显示系统各方面的行为,可把该描述制作成动画。此动画可对系统满足实际要求以及规定的要求提供了额外的置信度。

在下面的条款中将描述两种半形式化方法。

B.2.3.2 有限状态机/状态转换图

注:在GB/T 20438.3-2017表B.5、表B.7、表C.15和表C.17中引用了本技术/措施。

目的:建模、验证、规定或实施一个系统的控制结构。

描述:能够用它们的状态、它们的输入和它们的行动来描述许多系统。当处于状态S1时,在接受到输入1时,一个系统将会执行动作A并转换到状态S2。通过描述一个系统处于每个状态中时,每个输入导致该系统的动作,就能完整地描述一个系统。产生的系统模型叫做一个有限状态机(或有限状态自动机)。常常是把它画成一个所谓的状态转换图,此图显示系统怎样从一个状态转移到另一个状态;或者把它画成一个矩阵,在矩阵中,维数是状态和输入,矩阵元包含当系统处于给定状态中时,由接受输入导致的动作和新状态。

一个复杂系统或者具有一个自然结构的系统的情况可以在一个分层的有限状态机中反映出来。状态图是一种可以嵌套的状态转换图(目标的状态分为可以并行演化的两个或更多子状态，并且可以在某点重新组合为一个状态),这增加了状态转换标记法的表达能力,但在安全相关系统中也增加了不受欢迎的额外的复杂性。状态图有一个形式化的(数学上)规范,状态转换图可以适用于整个系统或某些对象或者它的元素。

可以检查表示成一个有限状态机的规范或设计的:

——完备性(在每个状态、对每个输入，系统必定有一个动作和新状态);

——致性(每个状态/输入对只描述一次状态改变);

——可达性(是否能通过任何输入序列从一个状态到达另一状态);以及

——没有无限循环或无出路状态，等等。

它们是关键系统的一些重要属性。很容易开发支持这些检查的工具,并且可以使用基于有限状态机的不同模型(形式化语言、佩特里(Petri)网、马尔可夫图形等等)。而且也存在能够自动生成测试用例的算法,这些用例用于验证一个有限状态机实现或者制作一个有限状态机模型的动画。状态转换图和状态图被各种工具广泛支持,包括图表的绘制和检查.生成描述状态机执行的代码。

他们也可以用于失效概率的计算，参见B.6和C.6部分。

参考文献:

Introduction to Automata Theory,Languages,and Computation(3rd Edition).J.Hopcroft,R.Mot- wani,J.Ullman,Addison-Wesley Longman Publishing Co,2006,ISBN:0321462254

Sécurisation des architectures informatiques, Jean-Louis Boulanger,Hermès-Lavoisier.2009. ISBN:978-2-7462-1991-5

B.2.3.3 时间佩特里(Petri)网

注:在GB/T 20438.3-2017的表B.5.表B.7、表C.15和表C.17中引用了本技术/措施。

目的:通过分析和再设计模型化系统行为的有关方面、评估及尽可能地提高安全性和操作要求。描述:佩特里(Petri)网是一个有限状态自动机的特殊情况,属于图形理论模型一类,适用于在呈现并发性和有异步行为的系统中表示信息和控制流。

佩特里(Petri)网是一个位置和变迁网。位置可被“标记”或“不标记”。当输入该网的所有输入位置被标记时,就“使能”一次变迁。当使能时,就允许(而不是强迫)“触发”。如果它触发,引起变迁的输入位置就变成未标记的了,并且代之以变迁产生的每个输出位置被标记。

在模型中可把潜在的危险表示成特定的状态(标记)。可把佩特里(Petri)网模型扩展成描述系统的时间特性。虽然“传统的”佩特里(Petri)网集中在控制流方面,已经提出了把数据流包括到模型中去的几种扩展方案。

这些也对执行蒙特卡罗模拟提供有效的支持,以实现失效概率的计算，参见B.6.6.8。

参考文献:

Timed Petri Nets:Theory and Application.Jiacun Wang,Springer,1998,ISBN 0792382706

Sécurisation des architectures informatiques. Jean-Louis Boulanger,Hermès-Lavoisier, 2009, ISBN:978-2-7462-1991-5

来源：小贾科技论