（中國船舶重工集團(tuán)公司第723研究所 揚(yáng)州 225001）

1 引言

本文主要針對軟件安全性需求建模進(jìn)行研究，建立基于四變量模型的軟件安全性需求模型。首先簡要介紹了四變量模型的建模原理，論述了四變量模型中的四種關(guān)系，即REQ，NAT，IN，OUT關(guān)系，并在需求層面對軟件行為進(jìn)行簡要介紹［1］；然后針對現(xiàn)有四變量模型的不足進(jìn)行改進(jìn)研究，使得四變量模型更加適用于軟件的安全性需求提?。?］；最后運(yùn)用改進(jìn)的四變量模型進(jìn)行軟件的安全性需求建模［8］，并通過實(shí)例驗(yàn)證方法的可行性和有效性。

2 四變量模型概述

四變量模型是基于在系統(tǒng)需求層面上分析系統(tǒng)行為和軟件需求的思想［5，10］，其最早是被Parns和Madey等提出。多應(yīng)用于飛機(jī)控制設(shè)備、醫(yī)療設(shè)備、核反應(yīng)堆或者是汽車控制等領(lǐng)域中［11］。通常這些應(yīng)用可以運(yùn)用四變量模型進(jìn)行建模分析其各個組成部件的行為需求，既包括系統(tǒng)行為，也包括軟件行為。

四變量模型顧名思義，共有四種類型的變量，這四種變量分別為受監(jiān)控的變量、受控制的變量、輸入變量和輸出變量［3，12］。其中受監(jiān)控的變量是指系統(tǒng)能夠監(jiān)控的變量，如電壓、電流、汽車油門等；受控制的變量是指系統(tǒng)可以控制的變量，如飛機(jī)高度、汽車速度等；輸入變量是指受監(jiān)控變量的另一種表現(xiàn)形式，其主要用于軟件的輸入；輸出變量是指用于控制受控制的變量的變量，作為軟件輸出。另外，四變量模型又包含REQ、NAT、IN和OUT四種關(guān)系。REQ和NAT用于描述受監(jiān)控的變量和受控制變量的關(guān)系，即受監(jiān)控變量發(fā)生變化時，受控制的變量會發(fā)生相應(yīng)的變化；IN和OUT分別描述了受監(jiān)控變量和輸入變量之間的關(guān)系，受控制變量和輸出變量之間的關(guān)系［2］。

3 四變量模型改進(jìn)研究

現(xiàn)有的四變量模型的基本思想是通過受監(jiān)控的變量對受控制的變量進(jìn)行控制［6］。在這種思想的驅(qū)使下，模型的輸入往往要求互相正交，但是在實(shí)際工程應(yīng)用中，由于工程師的經(jīng)驗(yàn)等問題的限制，很難真正做到受監(jiān)控的變量彼此獨(dú)立，這種情況會造成模型的輸出結(jié)果出現(xiàn)相互沖突，彼此不相容。運(yùn)用到軟件安全性需求提取中，會造成需求沖突的結(jié)果［9］。為有效解決這種問題，本文提出對四變量模型進(jìn)行改進(jìn)。

在四變量建模中，本文將軟件安全性需求作為系統(tǒng)需求約束，即受監(jiān)控的變量，系統(tǒng)的安全性作為受控制的變量［4］，其數(shù)學(xué)關(guān)系表示為

其中Ri表示系統(tǒng)需求約束集合；Si是受控制的變量，表示系統(tǒng)狀態(tài)。為了方便研究，本文將人機(jī)交互系統(tǒng)的狀態(tài)定義為S0（安全狀態(tài)）和S1（不安全狀態(tài)）兩種。

在四變量模型中，關(guān)系REQ和關(guān)系NAT描述的是系統(tǒng)層面上的需求，實(shí)際上是將系統(tǒng)看成一個黑盒子，只關(guān)心系統(tǒng)的輸入和輸出，其數(shù)學(xué)關(guān)系表示為

為了保證模型的建立，很多研究者在進(jìn)行建模時往往竭盡所能地使模型的輸入正交化，這樣就可以保證模型的處理能力。但是在實(shí)際工程中，往往存在受監(jiān)控的變量不是獨(dú)立的，在進(jìn)行建模時，刻意的對受監(jiān)控的變量進(jìn)行正交化會造成需求的漏洞甚至需求沖突。

為了使四變量模型具有處理非正交受監(jiān)控的變量的能力，本文在原有模型的基礎(chǔ)上增加的受控制的變量對于受監(jiān)控變量的反饋機(jī)制。通過這種反饋機(jī)制的建立，使得模型的處理能力更強(qiáng)。經(jīng)過擴(kuò)展后的模型如圖1所示。

圖1 擴(kuò)展后的四變量模型

這種反饋機(jī)制其實(shí)就是通過對安全性約束的傳遞和繼承來實(shí)現(xiàn)的。下面通過數(shù)學(xué)函數(shù)的推理計(jì)算說明這個單元函數(shù)是如何通過反饋機(jī)制產(chǎn)生多元函數(shù)的。

對于原有的模型，其數(shù)學(xué)函數(shù)表達(dá)式就是：

其中，Mi表示受監(jiān)控的變量，Si表示受控制的變量。很明顯，表達(dá)式（4）是一種典型的單元函數(shù)，通過反饋機(jī)制的建立，使得下一個變量的輸入受到上一個變量的輸出的影響，為了使表達(dá)式的結(jié)果與系統(tǒng)狀態(tài)（S1和S0）區(qū)分開來，本節(jié)將Si換成yi來表示，即：

其中，Δy1表示受控制的變量y1對于受監(jiān)控的變量M2的反饋影響，同理，Δyi-1表示受控制的變量yi-1對于受監(jiān)控的變量Mi的反饋影響。通過式（5）、（6）、（7）、（8）四個表達(dá)式可知，這種反饋將單變量函數(shù)變成了多變量函數(shù)，這種變化在模型中表現(xiàn)為多因素失效模式共同作用下對于系統(tǒng)的影響，即表達(dá)式（4），至此，模型的多元函數(shù)演化完成。也證明了通過這種反饋機(jī)制能夠?qū)⒛Ｐ陀蓡我蛩胤治瞿芰ο蚨嘁蛩胤治瞿芰Φ霓D(zhuǎn)換。

擴(kuò)展后的模型的原理其實(shí)就是在一個受監(jiān)控的變量（一般是異常操作或失效）經(jīng)過模型的作用得到一個系統(tǒng)狀態(tài)。這個模型會受到單因素作用下的系統(tǒng)約束和環(huán)境約束，因此，得到的這個系統(tǒng)狀態(tài)理論上為安全狀態(tài)。同時在反饋機(jī)制的作用下，四變量模型仍然可以受到其他受監(jiān)控的變量的作用，其他受監(jiān)控的變量仍然會受到相應(yīng)的系統(tǒng)約束和環(huán)境約束，這個時候模型就同時受到兩種系統(tǒng)約束和環(huán)境約束的作用。如果這兩種約束有沖突或者發(fā)生了矛盾，則系統(tǒng)就會進(jìn)入不安全狀態(tài)。最終通過系統(tǒng)狀態(tài)的判斷，就能找出多因素作用下的系統(tǒng)安全性需求。通過圖形反映這種作用過程如圖2所示。

在圖2中，首先對四變量模型輸入一個受監(jiān)控的變量，同時模型受到系統(tǒng)和環(huán)境約束1的約束，在這種約束下模型產(chǎn)生了一個受控制的變量；然后判斷受控制的變量的狀態(tài)，如果受控制的變量為S1，即不安全狀態(tài)，則對軟件施加新的安全性約束，這種約束就是軟件的安全性需求，同時輸入新的受監(jiān)控的變量。如果受控制的變量為S0，即安全狀態(tài)，則直接輸入新的受監(jiān)控的變量。新的受監(jiān)控的變量作用于四變量模型時也會受到新的系統(tǒng)和環(huán)境約束，同時由于反饋機(jī)制的作用，使得原來的系統(tǒng)和環(huán)境約束仍然對四變量模型起作用，如果這兩種約束沒有沖突的話，則系統(tǒng)會進(jìn)入安全狀態(tài)，否則說明兩種約束有沖突或者覆蓋不全，因此需要提取新的安全性需求。這種過程反復(fù)迭代，就能實(shí)現(xiàn)四變量模型對于多因素需求的建模分析了。

圖2 擴(kuò)展后的四變量模型分析過程

4 實(shí)例驗(yàn)證

4.1 事故簡介

1993年北歐聯(lián)合航空SAS751航班因發(fā)動機(jī)控制軟件的邏輯缺陷而發(fā)生事故，事故發(fā)生的過程如下所示：1）飛機(jī)起飛時機(jī)翼積冰破裂，進(jìn)入引擎擊傷葉片，導(dǎo)致引擎喘振；2）機(jī)長降低引擎速度；3）ATR（automatic thrust restoration）自動推力復(fù)原系統(tǒng)啟動，右引擎轉(zhuǎn)為最大加力，導(dǎo)致右引擎喘振加劇最終損壞；4）ARTS（automatic reserve thrust system）自動預(yù)留推力系統(tǒng)啟動，左引擎轉(zhuǎn)為最大加力，導(dǎo)致左引擎喘振加劇損壞；5）飛機(jī)雙發(fā)失效墜毀。

其中ATR是防止飛機(jī)在爬升時飛行員為了降噪或其他因素，降低推力使速度過低。觸發(fā)條件：1）高度＞350 f（t106.6m），2）引擎推力＜爬升推力，3）飛機(jī)狀態(tài)為爬升。啟動后，ATR將特定引擎速度加至最大推力。ARTS是為了在起飛時引擎發(fā)生單發(fā)故障而導(dǎo)致推力不足提供的系統(tǒng)，其觸發(fā)條件是：左、右引擎發(fā)生單發(fā)故障。啟動后，ARTS將尚能提供推力的引擎加至最大推力。

4.2 安全性需求提取

4.2.1 單因素安全性需求

表1 單因素作用下發(fā)動機(jī)控制系統(tǒng)安全性需求

4.2.2 多因素安全性需求

表2 多因素作用下發(fā)動機(jī)控制系統(tǒng)安全性需求

通過上述建模分析可知，多因素安全性需求模型可以發(fā)現(xiàn)單因素安全性需求模型無法發(fā)現(xiàn)的需求缺陷，通過這種方法可以有效地尋找出現(xiàn)有事故發(fā)生的原因，因此也證明了本文所提方法的有效性。

5 結(jié)語

本文提出了一種基于四變量模型的軟件安全性需求提取技術(shù)，分析了現(xiàn)有四變量模型的缺點(diǎn)和不足，研究改進(jìn)了四變量模型，并成功將其運(yùn)用到軟件安全性需求提取中，通過實(shí)例驗(yàn)證了方法的正確性。

然而本文提出的方法仍然有一定的局限性，在軟件安全性需求的影響因素?cái)?shù)量有限的情況下，運(yùn)用本文的技術(shù)可以有效的解決問題；但是在面對軟件安全性需求的影響因素?cái)?shù)量極其龐大的情況下，很難通過這種方法逐個組合分析，有必要采取形式化的方法，借助于計(jì)算機(jī)的計(jì)算分析能力快速提取軟件安全性需求。