一種形式化建模中活性屬性轉(zhuǎn)化方法研究

張棋 謝健 尹小花

摘 要：現(xiàn)有的安全關(guān)鍵系統(tǒng)開發(fā)的方法一般是在系統(tǒng)開發(fā)后期使用測(cè)試的方法對(duì)系統(tǒng)需求進(jìn)行驗(yàn)證，這種方法一方面需要耗費(fèi)大量時(shí)間與人力，另一方面測(cè)試并不能保證系統(tǒng)中不存在錯(cuò)誤。使用形式化的開發(fā)方法可以將軟件需求添加到模型中，使用數(shù)學(xué)證明的方法來(lái)驗(yàn)證所要建立的系統(tǒng)是正確的，即在開發(fā)早期就能發(fā)現(xiàn)需求與系統(tǒng)設(shè)計(jì)間可能存在的問(wèn)題，能夠有效地減少后期發(fā)現(xiàn)錯(cuò)誤所帶來(lái)的損失。在現(xiàn)有需求工程方法KAOS方法轉(zhuǎn)化到Event-B模型的方法基礎(chǔ)上，對(duì)其中活性屬性丟失問(wèn)題進(jìn)行研究，并給出了解決方法。

關(guān)鍵字：安全關(guān)鍵系統(tǒng)；KAOS；Event-B；活性；模型檢測(cè)

中圖法分類號(hào)：TP311 文獻(xiàn)標(biāo)識(shí)碼：A

Abstract： The traditional verification method of safety-critical system usually happened in the late stage of system development.On one hand，test stage requires a lot of time and effort，moreover，traditional test technique does not guarantee that there is no error in the system.On the other hand，formal development methods use mathematic language to describe requirements，and then use various model checking methods to prove that the model which contains properties of requirements is correct.So we can find design error in early development stage，and this can reduce the losses caused by late errors.In this paper，we discuss the deletion of liveness property in several translation method from goal-oriented method to Event-B method，then we give a solution.

Keywords：safety-critical system；KAOS；Event-B；liveness；model checking

1 引 言

安全關(guān)鍵系統(tǒng)是指系統(tǒng)運(yùn)行錯(cuò)誤會(huì)導(dǎo)致一系列危及生命財(cái)產(chǎn)安全等后果的計(jì)算機(jī)系統(tǒng)。常見的安全關(guān)鍵系統(tǒng)如車載自動(dòng)駕駛系統(tǒng)、醫(yī)療系統(tǒng)、航空控制系統(tǒng)等，這些系統(tǒng)在運(yùn)行過(guò)程中一旦發(fā)生錯(cuò)誤，造成的潛在危害往往是難以預(yù)估的[2]。因此，如何確保安全關(guān)鍵系統(tǒng)在運(yùn)行過(guò)程中正確行使其功能是目前軟件工程領(lǐng)域中研究的一個(gè)熱點(diǎn)。

在軟件工程領(lǐng)域中，形式化方法通過(guò)使用嚴(yán)格數(shù)學(xué)語(yǔ)言對(duì)需求進(jìn)行描述和建模，并且使用證明的方法驗(yàn)證需求和軟件模型之間的一致性和正確性。對(duì)于安全關(guān)鍵系統(tǒng)開發(fā)，使用形式化的語(yǔ)言來(lái)描述文本需求有助于消除自然語(yǔ)言的二義性，提高需求規(guī)范的準(zhǔn)確性。Event-B是一種基于一階邏輯和集合論的用于對(duì)需求進(jìn)行規(guī)約驗(yàn)證的形式化建模方法[1]。精化是Event-B區(qū)別于其它形式化方法的主要特征，即根據(jù)需求逐步向模型中添加細(xì)節(jié)使其完善。同時(shí)，早期模型中已經(jīng)被證明的安全性屬性在后續(xù)精化過(guò)程中可以得到保持。

然而，由于使用Event-B方法時(shí)需要從普通文本需求中獲取形式化的需求規(guī)范，對(duì)開發(fā)人員的專業(yè)背景要求較高。針對(duì)這一問(wèn)題，目前常用方法是使用需求工程方法對(duì)文本需求進(jìn)行預(yù)處理，將復(fù)雜需求分解成若干子需求，并且以半形式化方式進(jìn)行表達(dá)，然后將半形式化的需求規(guī)范轉(zhuǎn)化到Event-B模型中，通過(guò)這種方式可以有效降低需求規(guī)范的獲取難度。KAOS方法是一種經(jīng)典的面向目標(biāo)的需求工程方法，現(xiàn)有的研究是將KAOS方法中的目標(biāo)模型（goalmodel）轉(zhuǎn)換到Event-B組件中，如[3，4，6，10]。然而，這些方法都只是將目標(biāo)模型中的功能性需求及安全屬性轉(zhuǎn)到Event-B中，由于目標(biāo)模型中的目標(biāo)（goal）同樣表達(dá)了活性屬性，使得現(xiàn)有的方法在轉(zhuǎn)化過(guò)程中會(huì)出現(xiàn)活性屬性丟失的問(wèn)題[5，7，9]。本文在現(xiàn)有方法的基礎(chǔ)上，給出了目標(biāo)模型轉(zhuǎn)化到Event-B模型的過(guò)程中保持其活性屬性的方法。

結(jié)構(gòu)如下：第2節(jié)介紹KAOS方法中的目標(biāo)模型和Event-B的相關(guān)理論知識(shí)；第3節(jié)給出目標(biāo)模型中目標(biāo)的活性屬性到Event-B模型的相關(guān)轉(zhuǎn)化規(guī)則；第4節(jié)通過(guò)電梯實(shí)例介紹本文方法的有效性；第5節(jié)總結(jié)及未來(lái)工作的展望。

2 相關(guān)理論

2.1 KAOS方法

KAOS方法是一種面向目標(biāo)建模和分析的需求工程方法[8]。KAOS方法包含5種模型用于描述需求文本，本文主要研究其中的核心模型，即目標(biāo)模型（goalmodel）。在目標(biāo)模型中，目標(biāo)（goal）定義了系統(tǒng)為了實(shí)現(xiàn)對(duì)應(yīng)需求應(yīng)該完成的功能，可以分為實(shí)現(xiàn)目標(biāo)（achievegoal）和維持目標(biāo)（maintaingoal），分別表示功能性需求和安全性需求。實(shí)現(xiàn)目標(biāo)是指預(yù)期系統(tǒng)最終將要實(shí)現(xiàn)的屬性，形如：{If （Cur_Condition） then eventually （Tar_Condtion）}。維持目標(biāo)則是指在某些條件下系統(tǒng)中定義的需要一直保持的屬性，形如{If （CurrentCondition） then always not （BadCondition）}。

在目標(biāo)模型中，上層的抽象目標(biāo)可以分解精化為若干個(gè)子目標(biāo)，子目標(biāo)和上層抽象目標(biāo)之間通過(guò)三種關(guān)系聯(lián)系，分別為AND分解，OR分解，MileStone分解。

其中，AND分解表示當(dāng)且僅當(dāng)所有子目標(biāo)實(shí)現(xiàn)時(shí)，上層抽象目標(biāo)可以被滿足；OR分解表示子目標(biāo)中的一個(gè)實(shí)現(xiàn)時(shí)，上層抽象目標(biāo)可以被滿足；MileStone分解則表示子目標(biāo)按照一定次序?qū)崿F(xiàn)時(shí)，上層抽象目標(biāo)可以被滿足。

2.2 Event-B方法

為了驗(yàn)證模型中的屬性是否滿足需求規(guī)約，以及精化后的模型與上一層模型是否一致，Event-B在建模過(guò)程中需要對(duì)一些證明義務(wù)（proofobligations）進(jìn)行證明。這些證明義務(wù)主要包括不變式保持（INV）、無(wú)死鎖性（DLF）、膠合不變式。INV表示當(dāng)前模型中的事件所引起的狀態(tài)變遷應(yīng)該滿足不變式的要求，DLF要求模型中不存在死鎖，膠合不變式則表示精化后模型中的事件與抽象模型應(yīng)該保持一致。

3 目標(biāo)中的活性屬性到Event-B中的表達(dá)

在2.1節(jié)中，目標(biāo)goal分為兩種類型，分別為實(shí)現(xiàn)目標(biāo)和維持目標(biāo)，目前常用的轉(zhuǎn)化方法中如[3，4，6，10]一般是直接將實(shí)現(xiàn)目標(biāo)顯式地轉(zhuǎn)化到Event-B中的事件event中，即每一個(gè)目標(biāo)對(duì)應(yīng)于Event-B模型中的一個(gè)事件。然而，實(shí)現(xiàn)目標(biāo)同時(shí)也通過(guò)eventually修飾符來(lái)表達(dá)在將來(lái)某個(gè)時(shí)間點(diǎn)目標(biāo)狀態(tài)最終會(huì)到達(dá)這樣一種活性屬性?，F(xiàn)有的轉(zhuǎn)化方法一般忽略了實(shí)現(xiàn)目標(biāo)中的活性屬性的表達(dá)，考慮到目標(biāo)模型中的目標(biāo)ag可以被分解為多個(gè)子目標(biāo)如g1、g2，對(duì)應(yīng)轉(zhuǎn)化到Event-B模型中的事件evt1、evt2，存在這樣的一組事件執(zhí)行序列{evt1，evt1，…}，使得事件evt2無(wú)法得到執(zhí)行，ag中的目標(biāo)狀態(tài)Tar_Condition無(wú)法達(dá)到。可以看到，在轉(zhuǎn)化過(guò)程中，目標(biāo)ag中的活性屬性丟失。

在Event-B模型中，事件event表達(dá)狀態(tài)變遷行為的同時(shí)，自身具有三種不同的屬性{ordinary，convergent，anticipated}。Ordinary屬性表示事件的執(zhí)行次數(shù)不受約束，convergent屬性表示事件的執(zhí)行次數(shù)是收斂的，anticipated屬性表示事件的執(zhí)行次數(shù)不受約束，需要通過(guò)后續(xù)精化進(jìn)行約束。

事件的收斂通過(guò)變式variant進(jìn)行約束，變式是一組包含常數(shù)（x∈N）或有限集合（x∈P（α））的表達(dá)式。變式會(huì)隨著convergent事件的執(zhí)行遞減，當(dāng)變式的值為零或集合為空時(shí)，convergent事件在后續(xù)事件鏈中停止執(zhí)行。

4 結(jié)束語(yǔ)

使用KAOS方法將文本需求進(jìn)行分解建立目標(biāo)模型，并且將需求改寫轉(zhuǎn)化到Event-B模型中對(duì)應(yīng)元素，可以有效減少開發(fā)人員的工作量。目前現(xiàn)有的方法在轉(zhuǎn)換過(guò)程中只考慮到需求中的安全性屬性和功能性屬性，對(duì)活性屬性的轉(zhuǎn)化有所缺失。本文在現(xiàn)有方法的基礎(chǔ)上給出了將目標(biāo)模型中目標(biāo)的活性屬性添加到Event-B模型的方法，并且結(jié)合電梯實(shí)例說(shuō)明了該方法的有效性。

由于在Event-B的精化過(guò)程中，已經(jīng)標(biāo)記為convergent屬性的事件可能會(huì)在精化過(guò)程中分解為若干子事件，導(dǎo)致之前保持的活性屬性可能丟失，因此在之后的研究中將會(huì)關(guān)注Event-B精化過(guò)程中的活性屬性保持研究。

參考文獻(xiàn)

[1] ABRIAL J R.Modeling in event-b：system and software engineering[M].Cambridge University press，New York，2010.

[2] 黃志球，徐丙鳳，闞雙龍.嵌入式機(jī)載軟件安全性分析標(biāo)準(zhǔn)、方法及工具研究綜述[J].軟件學(xué)報(bào)，2014，25（2）：200—218.

[3] LALEAU R，SEMMAK F，MATOUSSI A，et al.A first attempt to combine SysML requirements diagrams and B[J].Innevations in Systems & Softuonre Engineering，2010，6（1-2）：47-54.

[4] MATOUSSI A，GERVAIS F，LALEAU R.A goal-based approach to guide the design of an abstract Event-B specification[C]// IEEE International Conference on Engineering of Complex Computer Systems.IEEE，2011：139—148.

[5] SCHNEIDER S，TREHARNE H，WEHRHEIM H，et al.Managing LTL properties in Event-B refinement[J].Lecture Notes in Computer Science，2014，8739：221—237.

[6] Traichaiyaporn，Kriangkrai.Modeling correct safety requirements using KAOS and Event-B[D].Japan：JAIST，2013.

[7] HOANG T S，ABRIAL J R.Reasoning about Liveness Properties in Event-B[C]// International Conference on Formal Methods and Software Engineering.Springer-Verlag，2011：456—471.

[8] VAN LAMSWEERDE A.Goal-oriented requirements engineering：a guided tour[C]// IEEE International Symposium on Requirements Engineering，2001.Proceedings.IEEE，2001：249—262.

[9] HOANG T S，SCHNEIDER S，TREHARNE H，et al.Foundations for using linear temporal logic in Event-B refinement[J].Formal Aspects of Computing，2016，28（6）：1—27.

[10] AZIZ B，ARENAS A E，BICARREGUI J，et al.From goal-oriented requirements to Event-B specifications[J].The First NASA Formal Method Symposium，2009：96—105.