一種形式化建模中活性屬性轉化方法研究

張棋 謝健 尹小花

摘 要：現有的安全關鍵系統開發的方法一般是在系統開發后期使用測試的方法對系統需求進行驗證，這種方法一方面需要耗費大量時間與人力，另一方面測試并不能保證系統中不存在錯誤。使用形式化的開發方法可以將軟件需求添加到模型中，使用數學證明的方法來驗證所要建立的系統是正確的，即在開發早期就能發現需求與系統設計間可能存在的問題，能夠有效地減少后期發現錯誤所帶來的損失。在現有需求工程方法KAOS方法轉化到Event-B模型的方法基礎上，對其中活性屬性丟失問題進行研究，并給出了解決方法。

關鍵字：安全關鍵系統；KAOS；Event-B；活性；模型檢測

中圖法分類號：TP311 文獻標識碼：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 引 言

安全關鍵系統是指系統運行錯誤會導致一系列危及生命財產安全等后果的計算機系統。常見的安全關鍵系統如車載自動駕駛系統、醫療系統、航空控制系統等，這些系統在運行過程中一旦發生錯誤，造成的潛在危害往往是難以預估的[2]。因此，如何確保安全關鍵系統在運行過程中正確行使其功能是目前軟件工程領域中研究的一個熱點。

在軟件工程領域中，形式化方法通過使用嚴格數學語言對需求進行描述和建模，并且使用證明的方法驗證需求和軟件模型之間的一致性和正確性。對于安全關鍵系統開發，使用形式化的語言來描述文本需求有助于消除自然語言的二義性，提高需求規范的準確性。Event-B是一種基于一階邏輯和集合論的用于對需求進行規約驗證的形式化建模方法[1]。……