面向自然語言需求的驗證性質生成方法

李曉劼,楊志斌,王翰豐,周 勇,李 維

1(南京航空航天大學 計算機科學與技術學院,南京 211106)

2(高安全系統的軟件開發與驗證技術工信部重點實驗室,南京 211106)

3(航宇救生裝備有限公司,襄陽 441003)

0 引 言

安全關鍵軟件(Safety-critical Software,SCS)[1]是指應用于航空、航天、交通、能源等領域的安全關鍵系統中,若失效則可能導致災難性后果的一類軟件[2].安全關鍵系統和軟件的安全性、可靠性等需要通過軟件測試與驗證來保障.然而,傳統的系統模型驗證方法一般是將扁平化的整個模型轉換,直接進行驗證,由于SCS軟件狀態復雜,這種方法會導致系統狀態空間爆炸的問題.近年來,基于形式化規約的組合驗證方法(Contract-Based Compositional Verification)[3-5]成為安全關鍵軟件領域解決驗證狀態空間爆炸問題的國際前沿熱點.組合驗證方法利用軟件系統的組合結構對驗證問題進行分解,先驗證各子構件的性質,然后綜合推導出整個系統的性質,通過分而治之的思想解決狀態空間爆炸問題.使用組合驗證方法有兩大前提,即一個描述系統的操作和狀態的模型,以及該系統各個組件必須滿足的一組性質,二者的正確性都需要得到保障[6].

在建模方面,安全關鍵系統領域常用的建模語言主要包括 Modelica、SysML、UML Marte、AADL、 EAST-ADL、SCADE、Simulink、等.其中,AADL (Architecture Analysis &Design Language)[7]能夠以層次化的方式表達系統的軟硬件架構,使用基于行為附件(Behavior Annex) 表達構件正常功能行為,使用基于故障模型(Error Model Annex)表達構件在失效條件下的故障行為,以一體化的方式完整支持模型驅動建模和數據驅動建模.AADL 架構模型組合驗證方法和環境AGREE(Assume Guarantee Reasoning Environment)[8,9]通過AGREE Annex表達契約以支持組合驗證,可將形式化規約插入已有的AADL模型中,使用k-歸納法作為模型檢驗的底層算法,實現需求驗證、架構設計和架構驗證.豐富的表達能力和驗證機制使得 AADL 成為航空航天領域設計與驗證方法的一種重要選擇.

在模型驗證方面,系統驗證性質一般通過自然語言或形式化規約描述.自然語言便于在軟件系統設計過程中涉及的各個利益相關者之間簡潔地進行技術交流,但使用自然語言描述的需求可能是不完整的、不精確的、非正式的和模棱兩可的,并且不容易被設計和分析工具處理.形式化規約則相反,用精確的數學符號來表達設計需求,但難以掌握和使用.如何從自然語言需求文本中提取形式化的驗證性質成為組合驗證方法在安全關鍵系統領域有效使用的關鍵.現有的形式化規約提取工作可分為3類:1)基于模板等結構化語法的形式化規約生成方法:由人為預定義限定自然語言模板,在使用時,將自然語言需求重寫為模板表述的需求,再通過模板與形式化規約的對照規則生成正式規約,例如由Reinkemeier等人提出的面向汽車特定時間需求的需求規范語言RSL[10];2)基于自然語言處理技術的規約提取方法:使用文本預處理、語法語義分析、生成語法樹等自然語言處理技術對需求文本進行解析,得到形式化規約,如張時雨等人提出的面向物聯網領域基于自然語言語法樹的規約生成方法[11];3)基于機器學習的規則抽取方法:對特定領域數據集上事件規則進行抽取生成規約,如Kasenberg等人從馬爾可夫決策過程的行為軌跡推斷LTL規約[12]等.

然而,已有研究主要針對通用軟件領域,還較少考慮航空航天領域以及中文自然語言需求.針對這些問題,本文提出一種基于自然語言需求的AADL模型組合驗證性質自動生成方法,這種方法結合了模板語言與自然語言處理兩種方法的特點.首先給出基于限定自然語言(Restricted Natural Language,RNL)的契約生成方法,定義模式定義語言(Contract Pattern Language,CPL),將自然語言需求劃分為各種模式,每種模式下有相應句型,并給出CPL2AGREEANNEX轉換算法,將模式定義語言模板限定的自然語言需求轉換為AGREE Annex描述的形式化驗證性質;其次,提出一種面向模式定義語言的原子命題生成方法,主要步驟包括文本預處理、句子結構提取和生成原子命題,首先使用已有自然語言處理工具對文本進行預處理,然后給出句子結構提取方法,生成句法標準樹,通過句法樹得到原子命題,將提取到的原子命題替換CPL句型中的占位符,生成完整的用CPL表達的需求.本文設計并實現了相關工具,并將其應用于工業界實際案例,從而說明該方法的可用性和有效性.

本文的研究框架如圖1所示.第1節介紹研究背景.第2節介紹模式定義語言CPL以及CPL2AGREE ANNEX轉換算法.第3節給出面向模式定義語言的原子命題生成方法.第4節介紹本文開發的原型工具.第5節介紹本文的案例.第6節介紹相關工作.第7節是本文的總結和展望.

1 研究背景

1.1 AADL

架構分析和設計語言AADL通常用來構建系統架構模型,能夠標準、精確地對復雜嵌入式實時系統的軟件、硬件體系結構以及功能或者非功能屬性的設計和分析,能夠使用單一的模型將系統設計、分析、 驗證、代碼生成等重要的環節融合在統一的框架中.

AADL采用半形式化的建模概念,描述了復雜嵌入式系統的軟件、硬件架構和非功能屬性,包括不同的組件類型及組件間交互[13].組件之間的通信可以通過數據流、子程序調用或訪問共享變量來實現.AADL 建模語言具有可擴展能力,已有的擴展附件包括表達系統的軟硬件架構的行為附件(Behavior Annex)、表達構件在失效條件下的故障行為的故障模型(Error Model Annex)以及組合驗證方法和環境擴展附件AGREE Annex等.

1.2 AGREE

1.2.1 AGREE工具原理

假設保證推理環境(AGREE)用于對AADL模型進行組合驗證.AGREE將AADL模型和行為契約轉化成同步數據流編程語言,然后用模型檢查器對其進行分析.分析的過程按照體系結構分層進行組合執行,以便包含下一層次的組件來執行更高級別的分析.與單構件驗證相比,AGREE采用的組合分析方法可以允許分析擴大到更大的系統.

AGREE是構建在Eclipse上的OSATE AADL工具集的插件.首先通過解析器AGREE Parser對AGREE Annex 附件進行解析,生成用抽象語法樹AST表示的AGREE Program,這個AGREE的抽象語法樹通過分析插件AGREE Analysis Plugin 形成Lustre程序抽象語法樹,然后再用jKind模型檢查器進行驗證檢查.出現錯誤時,AGREE模型遵循模型檢查器jKind的標準將錯誤信息進行轉換,增加可跟蹤性信息,以便在向用戶顯示反例時可視化每個組件的活動錯誤信息.

1.2.2 AGREE Annex語法

AGREE工具支持將AGREE Annex插入AADL模型組件的描述中.AGREE Annex語句聲明如下:

Annex agree {?? -- agree declarations here…??};

AGREE共有Assume、Guarantee、Equation、Property、Constant、Node、Record、Real-time Patterns等語句類型,其中Real-time Patterns之下還有4種子類型,分別為WheneverStatement、RealTimeStatement、WhenStatement、ConditionStatement,AGREE Annex的使用對象可以是當前組件的特征、性質、和子組件,支持嵌套語句,因篇幅有限,具體格式在此不再贅述,請參考AGREE用戶手冊[14].頂層語句的語法描述如下:

AgreeSubclause ::= (SpecStatement)+ ; SpecStatement ::= ′assume′ STRING ′:′ Expr| PatternStatement ′;′ | ′guarantee′ STRING ′:′ Expr | PatternStatement ′;′ | ′assert′ (STRING ′:′)? Expr | PatternStatement ′;′ | EqStatement | PropertyStatement | ConstStatement | NodeDefExpr | RecordDefExpr | LemmaStatement; LemmaStatement ::= ′lemma′ STRING ′:′ Expr ′;′ EqStatement ::= ′eq′ Arg (′,′ Arg)? ′=′ Expr ′;′ ; PropertyStatement ::= ′property′ ID ′=′ Expr ′;′ ; ConstStatement ::= ′const′ ID ′:′ Type ′=′ Expr ′;′ ;

2 基于限定自然語言的契約生成方法

目前大多數軟件需求文檔都是采用自然語言編寫,而自然語言存在不完整、不精確、非形式化和二義性等問題,給軟件開發的系統驗證階段帶來很多不便,為了解決這樣的問題,本節將給出基于模式定義語言(Contract Patterns Language,簡稱CPL)的AGREE Annex驗證性質生成方法,給出模式定義語言的定義、需求模式類別、需求句式模板以及CPL2AGREEANNEX轉換算法.

圖2是CPL2AGREEANNEX方法總體流程圖,對于一條限定自然語言需求語句,首先根據句子中的關鍵字判斷其所屬的需求模式以及對應的句型模板;其次,通過原子命題生成方法獲取原子命題,將所得的原子命題公式填充至句型模板中,得到一條完整的CPL描述的需求;最后,通過轉換算法將CPL需求轉換為AGREE Annex驗證性質.這里要說明的是,本文中的限定自然語言需求是通過手工將自然語言需求文本中非正式、口語化的描述轉為較正式的表述方式,并刪除與驗證性質無關的描述所得.

圖2 CPL2AGREEANNEX方法流程圖Fig.2 Overview of CPL2AGREEANNEX

2.1 模式定義語言

本節提出基于自然語言需求的模式定義語言(Contract Pattern Language,CPL),提供一種從限定自然語言需求文本中提取驗證相關信息、并轉換為形式化驗證性質的方法.首先對自然語言文本加以半形式化約束,得到以CPL描述的需求,然后通過轉換算法,將其轉為AGREE Annex.

航空航天領域系統需求的模式可以劃分為功能模式、實時模式、概率模式和資源模式,每一種模式中包含一種或特定的需求句型,每種句型又表達了特定的系統需求.模式Pattern和契約模式定義語言的定義如下:

定義1.模式(Pattern)可以表示為一個二元組Pattern::=,其中,

1)Mode表示模式類別,屬于功能模式、實時模式、概率模式、資源模式之一;

2)Type表示句式,不同的需求模式下對應著不同的句式.其中,句式的基本元素如下,ID為標識符名稱,QID中“::”表示所屬關系,即ID2為ID1中的成員,NestedDotID表示嵌套ID.

QID::=ID1′::′ID2;NestedDotID::=ID(′.′NestedDotID)|ID;

句式中可包含如下的關系操作符和邏輯運算符,其中pre操作符表示組件前一時刻的狀態,->操作符用于初始化,=>操作符表示蘊含算子.

RelateOp::=′<′|′<=′|′>′|′>=′|′=′|′<>′|′!=′|′+′|′-′|′〔′|′/′|;LogicOp::=′pre′|′event′|′this′|′not′|′->′|′=>′|′and′|′or′;

由基本變量和運算符可以組合成如下所示的句式:

Expr::=ID|QID|NestedDotId|ID′(′Expr_List′)′|ε|Expr RelateOp Expr | Expr LogicOp Expr |IfElseStatement|VariableStatement|MultiEventStatement|WhenOccurStatement|WheneverholdStatement|WhenImplyStatement|DuringRaiseStatement|ConditionStatement|ProbabilityStatement|ResourceStatement;Expr_List::=Expr′,′Expr_List|Expr;

定義2.契約模式定義語言(Contract Pattern Language)為一個二元組,表示為CPL::=,其中:

1) C表示需要添加AGREE語句的AADL模型的構件集合.

2) P表示該組件具有某些特征的系統需求模式集合,P包含于Pattern.

其中,構件是AADL模型中的所有構件的構件類型聲明(Type)和構件實現(Implementation),包含軟硬件構件和系統構件.C中元素與P中元素是一對多的關系,即一個構件的需求可以分別對應到不同的模式.

2.2 需求模式和句型

定義1中的4種需求模式以及相應的句式是從600+條工業界實際需求中抽取得到,模式和句型具體如下:

2.2.1 功能模式

功能模式表達最直觀、基礎的功能需求,是構成其它模式句型的基礎,包括事件、觸發條件、變量之間的關系,也可擴展到多個事件序列、多個條件序列等復雜執行的情況.

1)條件句式

條件句式用于系統在準備執行某些操作前,判斷真假的語句,類似于C語言中的IF-ELSE語句的判斷條件,因此常與IF-ELSE結構同時使用.句式描述如下:

IfElseStatement::=′if′Expr ‘then’ Expr (‘else’ Expr)?|(‘else if’ Expr)?|ε;

條件句式在航空航天系統需求中應用廣泛,如描述系統中斷、故障自動處理等,如需求“如果連續收到20個信號則觸發中斷”則可以用條件句式描述如下:

if (get.signal().num=20)then set(System.state=INTERRUPT)--進行中斷操作

航空航天系統一些場景需進行模式切換,模式之間的切換對應著復雜的轉換條件與相關操作,如彈射系統需求“系統完成初始化后監測彈射啟動開關信號,若不滿足彈射控制模式進入條件則保持正常飛行模式,否則進入彈射控制模式”,則可以使用條件句式做出如下描述:

eq sm :int=init_MODE ->if System.GET_TS_SIGNAL then TS_MODE else FLYING_MODE;

2)變量關系句式

變量關系是指系統中存在較為復雜的變量之間的不等關系,主要是用于變量的賦值、計算.句式描述如下:

VariableStatement::=Expr (RelateOp Expr)?;

故障往往可以看作一類特殊事件,可以用變量關系句式描述安全關鍵軟件領域常用的故障或失效概念,如系統控制故障等設備故障以及通信超時等通信故障.如“若慣測模塊連續60ms未收到數據則為超時”中,可以將“超時”這一失效概念的定義如下:

const timeout_limit :int=60;

3)多個事件序列

用于描述兩個或多個事件的發生序列,句式描述如下:

MultiEventStatement::=event (‘and then’ event)?;

如“事件A、B、C按順序發生”則可以表示為:

event A and then event B and event C;

2.2.2 實時模式

實時模式是功能模式的擴展,在基礎語句上增加時間相關的描述,用于表達系統的實時行為,即在某個時間段內指定系統完成某些具體的操作.

1)when-occur句式

whenever E1 occurs E2 occurs/dose not occurs during [a,b]表示無論E1何時發生,E2將在閉區間[a,b]內某一時刻發生或不發生.句式描述如下:

WhenOccurStatement::=‘whenever’ Expr1 ‘occurs’Expr2 [‘dose not’] ‘occurs during’ [a,b];

對于需求“控制板在140ms內等待另一路控制板的同步信號,若收到則執行點火功能”表述如下:

if whenever controller.action() occurs get.signal() occurs during [0,140ms] then fire.on();

2)when-hold句式

whenever E1 occurs E2 holds during [a,b],無論E1何時發生,E2將在閉區間[a,b]內一直發生.句式描述如下:

WheneverholdStatement::=‘whenever’ Expr1 ‘occurs’Expr2 ‘holds during’ [a,b];

3)when-imply句式

whenever E occurs E1 implies E2 during [a,b],無論E何時發生,E1=>E2將在閉區間[a,b]內一直發生.句式描述如下:

WhenImplyStatement::=‘whenever’ Expr ‘occurs’Expr1 ‘implies’ Expr2 ‘during’ [a,b];

4)during-raise句式

[E1] during [a,b] raises [E2] 表示E1在閉區間[a,b]一直保持,E1結束后立刻觸發E2.句式描述如下:

DuringRaiseStatement::= Expr1 ‘during’ [a,b] ‘raises’Expr2 ;

5)周期句式

condition C1,E1 occurs each T表示在條件C1成立的前提下,E1在每個T周期內發生一次.句式描述如下:

ConditionStatement::=‘condition’ ExprC ‘,’ ExprE ‘occurs each’ T;

2.2.3 概率模式

與實時模式類似,概率模式是功能模式的擴展,增加了具有概率量化的約束,一般用于表達故障、失效的發生概率.用when-hold句式說明,“whenever E1 occurs E2 holds during following with a probability p”表示“無論E1何時發生,E2將在時間區間[a,b]內一直保持的概率大于p”.句式描述如下:

ProbabilityStatement::=Expr′with a probability′ number;

2.2.4 資源模式

資源模式是功能模式的擴展,用于表達對系統資源的約束[18],常見形式為定義硬件屬性、性能等.可以使用變量關系句式定義簡單的資源描述:

Stack_Size=1024 Bytes; --對棧內存的限制Compute_Execution_Time=10 us ; --對CPU的約束

也可以以區間的形式對系統資源加以限定,描述如下:

ResourceStatement::=Expr ′with a resource_consumption′ [a,b];

為了方便讀者理解這些句式,表1給出實時模式、概率模式下部分語句的圖形化語義.

表1 部分語句的圖形語義Table 1 Graphical semantics of some statements

2.3 CPL2AGREEANNEX轉換算法

對于CPL中不帶時間約束的功能模式等需求可以直接對應到不含時序算子的基本命題邏輯公式.轉換算法如下:

Algorithm1 Transformation from CPL2AGREE AnnexInput:CPLOutput:AGREE Annex1.for each Component c in CPL.getComponents do2. for each Pattern p in CPL.getPatterns do3. If(p==RTReq) then4. for each Type t in p.getType do5. for each l in t.getSentence do6. call_sentenceTemplate();7. end for8. end for9. else10. …… 11. end If12. end for 13.end for

對于CPL中包含時間約束的實時模式,算法1中第6行的函數call_sentenceTemplate()需要通過添加不變量來表達對時間的計算,生成帶有時序斷言的狀態邏輯公式.一般的做法是在AADL模型頂層系統的AGREE Annex中定義一個表示時間的變量來表示時間觀察者

eq T:int=0->pre(T)+1;

T代表系統時鐘,pre 是同步語言特殊操作,即獲得前一時刻變量的取值,先初始化T為0表示系統開始時間,然后每個時鐘執行一步,T計數加1.表2以實時模式(1)、模式(4)兩種語句說明時鐘的轉換方式.

表2 時鐘轉換示例Table 2 Clock conversion example

3 面向模式定義語言的原子命題生成方法

由于手工填充CPL句型的關鍵字存在工作量大、錯誤率高等缺點,本文提出面向模式定義語言的原子命題生成方法,用于提取需求中的關鍵詞,提高轉換效率.

給定一條中文自然語言需求,首先對其進行文本預處理,得到句子中的依存關系;其次提取句子結構,構建標準句法樹;最后,根據句法樹生成面向CPL的原子命題.另外,將給出一個原子命題提取示例.

3.1 文本預處理

使用已有的自然語言處理工具HanLP完成文本預處理,首先依據輸入的開始以及結束索引從原始需求語句中提取出當前處理的子句,然后對獲得的子句進行依存句法分析,完成分詞、詞性標注,獲得當前子句的依存句法樹.

3.2 句子結構提取

3.2.1 句子結構優先級

研究人員從工業界實際需求中抽取出8種句子結構,表3給出8種句子結構的語義和優先級,當多種句型嵌套時,優先級最高的句子結構即為當前處理子句的主要句子結構.

表3 句子結構Table 3 Sentence structure

3.2.2 依存關系

一種句子結構僅對應特定幾類依存關系,本文通過分析大量實際需求語句,總結出句子結構與句子依存關系的對照表,如表4所示.

表4 依存關系對照Table 4 Dependency relation comparison

3.2.3 基于依存關系的句子結構提取規則

通過對句子的依存關系進行關鍵字匹配,找到對應的句子結構.在遍歷依存句法樹時,根據預處理得到的依存關系,匹配可能出現的關鍵字,若匹配到了該依存關系可能對應的優先級最高的句型的關鍵字,則創建非葉子節點保存相關信息;若匹配到優先級較低的關鍵字,則需判斷之后是否存在高優先級的關鍵字,若不存在則創建非葉子節點保存相關信息,否則不進行任何操作.表5為句型關鍵字對照表,表6給出時間約束對應的關鍵字.

表5 句型關鍵字Table 5 Keyword of sentence pattern

表6 時間約束關鍵字Table 6 Keyword of time constraint

3.3 原子命題生成

原子命題提取是在識別出處理的語句是簡單句時執行的操作,本步驟從原始的簡單句需求中提取需求語句中的時間約束、全域標識符主語、謂語、賓語,按照主謂賓的順序對語句進行重新組織,從而生成可用于填充CPL模板的原子命題.

本文采用正則表達式提取時間約束,分別匹配時間約束中的數字、中文單位以及英文單位;由于全域標識符只有特定的若干關鍵字,所以直接使用字符串匹配來提取全域標識符;根據依存句法分析中各詞與核心詞的關系進行主謂賓提取,與核心詞構成主謂關系或定中關系的名詞視為主語,與核心詞構成動賓關系的詞語視為賓語,而核心詞即視為謂語.

3.4 原子命題提取示例

這里以彈射系統需求“系統初始化及上電自檢完成后,若有地檢控制開關信號且握手成功,則系統進入地檢模式.”作為示例進行原子命題提取.在句子中匹配到“后,”,則該條需求屬于1型條件句,再向下遞歸,兩個子句中分別匹配到“及”和“若…則…”,即內部并列句和2型條件句的關鍵字,再對子句進行語法樹生成,直至葉子節點所記錄子句的均為簡單句,即為所求的原子命題.標注句法樹如圖3所示.

圖3 標注句法樹案例Fig.3 Example of annotation syntax tree

4 原型工具

4.1 總體框架

RNL2PRO工具是基于開源的AADL模型建模和驗證平臺OSATE[15]開發的插件項目,借助OSATE語法分析功能解析已有的AADL模型,實現從自然語言需求文本中提取驗證性質,并轉化為AADL模型驗證工具AGREE可識別的AGREE Annex語句.工具分為原子命題生成和CPL2AGREEANNEX兩個模塊,圖4為工具的總體框架.

圖4 工具總體框架Fig.4 Framework of the RNL2PRO tool

4.2 原子命題生成工具

原子命題生成工具分為文件I/O處理、原子命題生成和目標語言轉換3個模塊,實現效果如圖5所示.

圖5 原子命題生成工具Fig.5 Tool of atomic propositions generation

用戶單擊最左側“上傳文件”按鈕上傳需求文檔后將在①面板處顯示,可以選擇某條需求,也可以在中間②面板處手動輸入;點擊“確定”按鈕,③中顯示該條需求中原子命題的連接方式,④中顯示生成的原子命題;在⑤的下拉框選擇對應的原子命題并輸入英文描述,可將中文原子命題替換為英文.本工具由4.3節介紹的CPL2AGREEANNEX工具調用,點擊“生成公式”按鈕可將生成的原子命題傳回.表7為原子命題生成工具的代碼行數統計.

表7 原子命題生成工具代碼行數Table 7 Code lines of atomic proposition generation tool

4.3 CPL2AGREEANNEX工具

CPL2AGREEANNEX工具包括句型模板選擇、CPL語句生成、語句轉換和文件處理4個模塊.用戶右鍵單擊*.aadl文件選擇“驗證性質生成”啟動插件后,工具將自動獲取系統的各組件,選擇待驗證組件之后進入圖6所示的界面.

圖6 CPL2AGREEANNEX工具Fig.6 Tool of CPL2AGREEANNEX

用戶在①中文本框輸入自然語言需求,選擇自然語言需求對應的CPL句型后點擊②中的“提取原子命題”按鈕將啟動原子命題生成工具,在原子命題生成工具完成后單擊“顯示”按鈕,提取到的原子命題將顯示在對應的文本框內.點擊②中“生成模板”按鈕則將根據選擇的CPL句型使能④中模板的相應位置,用戶通過選擇下拉框填充模板后,點擊⑥中的“生成Assume”按鈕,工具將自動組裝句型模板和原子命題,并轉化為AGREE Annex語句.工具下半部分為Guarantee生成區域,操作方式與生成Assume相同.最后單擊“導入AADL模型”按鈕則可以將生成的形式化驗證性質插入原AADL模型的適當位置.表8為CPL2AGREEANNEX工具的代碼行數統計.

表8 CPL2AGREEANNEX工具行數Table 8 Code lines of CPL2AGREEANNEX tool

5 實驗評估

本節將對航空航天領域彈射座椅子系統進行系統驗證,首先建立彈射座椅系統的AADL模型,并將用本文的方法從其需求文本中提取驗證性質,完成模型驗證.

5.1 彈射系統簡介

本文根據系統需求中對各組件及其接口的描述建立了彈射座椅系統的AADL體系結構模型.彈射座椅系統軟件部分由控制器監控模塊、程序控制模塊、彈射啟動模塊、座椅姿態控制模塊組成,主要功能包括數據源接收判斷、彈射啟動響應及健康管理.系統通過采集、監測人-椅系統多種不同的彈射離機狀態參數以及彈射出艙后飛行運動參數,根據系統內嵌多模式/多模式數字彈射控制模型,實時地自動選擇彈射控制程序,實現多模式的控制方式.

5.2 彈射座椅系統建模與驗證性質生成

彈射座椅需求文檔共有514條與驗證性質相關的需求,本實驗首先通過手工對自由文本的非正式表述加以限制并刪除文本中與驗證性質無關的內容,再將每一條需求先轉化為CPL表達式,通過轉化算法將CPL表達式轉化為AGREE Annex語句.本文從中選出一條典型需求為例,對于自然語言需求“控制板在140ms內等待另一路控制板的同步信號,若收到則執行點火功能”,使用CPL則可以表達如下:

if (whenever controller.action() occursget.signal() occurs during [0,140ms])then fire.on();

本文的工具能夠將上述CPL表達式自動轉換為AGREE Annex描述的形式化驗證性質:

eq Tnow:int= 0->pre(v) +1;assert “時鐘同步”:Tnow =T;guarantee “實時模式”:True->(controller.ACTION)&&get.SIGNAL&&(0<= T and T <=140)=> fire.on());

5.3 實驗結果

研究人員使用第5節介紹的工具對514條自然語言需求進行驗證性質的提取,其中,大多數驗證性質可以被正確提取并轉換為AGREE Annex描述,結果如表9所示.

表9 實驗結果Table 9 Experimental result

這個實驗結果表明當前的驗證性質生成方法尚存在以下幾個問題:

1)原子命題生成部分可識別句型、關鍵字等有待擴充;

2)實時模式和概率模式的句型模板應當得以擴充,當前句型模板尚不完善;

3)當前的處理方法在處理長難句時出錯概率稍大,提取正確率相對較低;

4)需求樣本數量較小,特別是資源模式需求語句,應當擴大樣本總量.

綜上所述,本文介紹的方法及工具能夠從自然語言需求文本中提取大多數驗證性質并正確轉換為AGREE Annex語句,在工業界實際操作時可以減少大部分工作量,但提取原子命題的自然語言處理算法仍需優化,且需要豐富句型模板以覆蓋更多的實際需求,目前,句型模板的提取主要依賴手工完成,適應性較差,這些缺陷都有待進一步改進.

6 相關工作

形式化驗證是保障安全關鍵軟件安全性、可靠性有效的手段,使用這一方法的前提是具有描述系統的操作和狀態的模型以及該系統的每個實現必須滿足的一組屬性[6].如何從需求從獲取屬性并且將其轉化為可以被驗證工具接受的形式化規約,成為形式化驗證領域研究的重點和難點.當前從自然語言需求文本中提取形式化規約的工作主要有以下幾類:

1)基于模板等結構化語法的形式化規約生成方法:由領域專家和計算機領域人員共同參與設置限定自然語言模板,通過解析自然語言文本獲取原子命題,填充模板中的占位符,并定義該模板到邏輯語言正式規約的轉換算法,得到形式化規約.Dwyer等人從廣泛應用領域的需求文本中抽取了最初的需求模板[16],對系統有限狀態模型中允許的狀態/事件序列的常見要求的廣義描述,并將自然語言需求按照其描述的側重點劃分為需求模式,給出最初的模式組織方式PSP(Property Specification Patterns)[17].Dwyer在后續論文中對模式類別進行細化,將模式劃分為定性、實時、概率3類,詳細介紹了定性模式,并將可映射的邏輯語言增加到3種[18].在Dwyer工作的基礎上,文獻[19,20]著重闡述PSP中的實時模式,文獻[21]對概率模式展開詳細說明.Autili等人[22]將定性模型又分為發生模式和順序模式,通過對已有的需求模式進行組合、限定作用域,得到40種新的子模式,以UML的形式給出了各子模式的繼承、泛化等關系,并將可映射的邏輯語言增加至6種.以上的工作逐步完善了通用領域的需求模式目錄.然而PSP主要針對通用領域的需求,應用于一些專用領域自然語言需求文本時有所不足,于是一些工作針對專用領域需求文本提出如汽車領域的部分需求格外強調實時性與安全性,需采用定時增強描述語言(TADL)作為形式化驗證的邏輯語言,而現有的模板還未涉及,Reinkemeier等人則提出了面向汽車特定時間需求的需求規范語言RSL,并給出RSL到TADL的映射規則[10].合同規范語言CSL的則更關注將來時態,用于對一系列商定的未來事件進行規約,監控事件發生及發生之后的情況[23].目標合同規范語言GCSL[13]是對象約束語言(OCL)和契約模式“SPEED”[24]的組合,在CSL的基礎上加強了關于組件實時行為的表達.

2)基于自然語言處理的規約提取方法:這類方法使用文本預處理、語法語義分析、生成語法樹等自然語言處理技術對需求文本進行解析,得到形式化規約.張時雨等人提出一種面向物聯網領域基于自然語言處理技術的建模和規約生成方法[11],使用 NLP 構造初始解析樹及中間表示,利用語義模板為中間表示中的子句生成原子命題,同時設計了一個原子命題到完整LTL規約的轉換算法[25].王小兵等人提出了一個自然語言到時間邏輯公式的自動轉換框架[26],使用CoreNLP工具對結構化英語文本進行句子成分提出,然后提取原子命題,并根據時態、副詞和介詞短語推斷每個原子命題的時態運算符,生成語法樹并根據語法樹生成PPTL公式,再通過轉換規則映射到LTL邏輯公式.Ghosh等人提出自然語言需求規約自動化提取方法,針對安全關鍵系統,將NL需求先轉換到中間表示,并設計了形式化分析復合框架,將中間表示映射到SAL模型和LTL[27].Lignos等人則使用了多個 NLP 技術進行句法分析和語義分析,實現了邏輯命題與自然語言的雙向映射[28].

3)基于機器學習的規則抽取方法:不同于上面兩種方法需要人為定義模板或轉換規則,本類方法通過監督學習等手段自動生成.文獻[29,30]提出了結合數據挖掘和寄存器傳輸級別(RTL)設計靜態分析自動生成斷言的GoldMine方法,首先模擬了RTL設計,以生成關于該過程的動態行為的數據.然后挖掘生成的數據,挖掘出可能是不變量的“候選斷言”,設計了一種決策樹監督學習算法和一種覆蓋引導挖掘算法來生成高質量的斷言,并通過正式的驗證過濾出虛假的候選.被正式引擎證明為正確的斷言是系統不變量.然后,通過一個作為反饋給數據挖掘引擎的設計器排名過程對這些數據進行評估.Kasenberg等人考慮從馬爾可夫決策過程的行為軌跡推斷LTL規約[12].Harris[31]提出利用監督學習生成轉換規則的方法[32],在此基礎上先將NL文本轉化為邏輯表達式,再轉化為形式化規約,這兩步均采用監督學習的方法,分別生成模板和模板與邏輯符號間的對應規則.

7 結論與展望

本文提出一種基于自然語言需求的AADL模型驗證性質自動生成方法,定義了模式定義語言CPL,給出CPL句型模板,并用自然語言處理技術提取填充模板的原子命題;設計實現了AGREE Annex形式化規約自動生成工具,并將本文方法應用于實際工業界案例中,建立了航空器彈射座椅系統的AADL模型,從其需求中提取驗證性質,完成模型驗證.結果表明,本方法能有效提取自然語言需求中的驗證性質,并正確轉換為AGREE Annex語句,能夠幫助軟件工程師減少大部分工作量.

未來將考慮優化原子命題提取算法,并引入機器學習算法自動提取句型模板,并考慮將句型模板映射到AGREE Annex的底層邏輯P-LTL,從而更好的說明轉換算法的正確性和完整性.