[發明專利]面向CPS的μ演算實數值性能評價方法

在審

• 申請號: 202110227457.6
• 申請日: 2021-03-01
• 公開（公告）號: CN113051714A
• 公開（公告）日: 2021-06-29
• 發明（設計）人: 朱一峰;曹子寧;王?？?/a>
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F30/20
• 分類號: G06F30/20;G06F111/08
• 代理公司: 暫無信息
• 代理人: 暫無信息

本發明公開了面向CPS的μ演算實數值性能評價方法。本發明使用Kripke結構作為基本的遷移系統進行解釋，并在此基礎上提出帶有原子函數的Kripke結構。本發明通過從集合推廣至函數的方法將μ演算的輸出值從布爾域推廣至實數域，從而實現性能評價方法。本發明在推廣至函數值的μ演算的基礎上提出了新的性能評價語言??μR。最后通過Tarski不動點定理證明此性能評價語言中不動點的存在性，即確保其合理性，以保證后續改進以及驗證工作的正確性。

技術領域

本發明公開了一種面向CPS的μ演算實數值性能評價方法，主要用于對CPS使用形式化驗證的方法進行系統驗證，并通過輸出為實數值的性能評價語言進行系統度量分析。

背景技術

信息物理融合系統(CPS)是基于行為離散、時間連續的復雜混成系統，同時在實際應用中，還可能夾雜著不確定性、資源消耗性等各種附帶信息的屬性。這種混成系統在現實生活中受到了廣泛的運用，而在受到人們廣泛運用的同時，混成系統的安全性和可靠性也變得尤為重要。因此，保證這類混成系統的安全性和可靠性也成為了目前的主要研究方向。模型檢測技術是一個基于有限狀態的形式化驗證技術，通過對系統進行形式化的建模，并采用可以描述形式化模型的相應邏輯語言來表達需要驗證的性質，并將性質由公式的形式所表達出來，通過模型檢測算法進行相應的驗證。目前模型檢測技術通常使用的經典模型有有限狀態自動機、時間自動機、概率自動機、混成自動機以及進程代數CSP(Communication Sequential Process)、CCS(Calculus of Communicating Systems)等，經典時序邏輯有線性時序邏輯 LTL(Linear Temporal Logic)和計算樹邏輯CTL(Computation Tree Logic)。

針對CPS的不確定性和時間消耗性，經典的LTL和CTL時序邏輯語言沒有足夠的能力刻畫相應的性質，因此有學者在前兩者的基礎上添加了概率算子和時間算子，提出了概率計算樹邏輯PCTL(Probabilistic Computation Tree Logic)、概率線性時序邏輯PLTL(Linear Temporal Logic with Probability)以及時間計算樹邏輯TCTL(TimedComputation Tree Logic)，并分別給出了模型檢測算法。然而即使增加了時間或概率算子，能夠刻畫出相應的概率性質和時間性質，但仍然無法對具體的實數值進行刻畫。換言之，傳統的模型檢測技術僅僅是對所要驗證的一個性質公式進行形式化驗證，而后得出相應的布爾值，即True或False，而并不能得到滿足某個性質的條件下，會花費多少時間，或者以多大/小的概率能夠滿足該性質。為了解決這類傳統的時序邏輯語言遇到的問題，本發明通過已有的性能評價語言CTML (Computation Tree Measurement Language)以及傳統的μ演算提出了一個表達能力較強的的性能評價語言——μR。

發明內容

信息物理融合系統存在著不確定性且伴隨資源消耗。由于傳統的μ演算無法描述需要輸出實數值的性質，而其表達能力卻非常強大，因此本發明在其基礎上，與性能評價方法相結合，將μ演算通過函數的方法轉換至性能評價方法中。

本發明是一種面向CPS的μ演算實數值性能評價方法，主要包括以下步驟：

步驟1：對Kripke結構引入原子函數，有以下一個元組(AF)

AF是原子函數的有限集合，每一個狀態都有與之相對應的原子函數，即該狀態下原子命題滿足時，其函數取值為1，否則為0。

步驟2：將μ演算的語義解釋從狀態集合推廣至{0，1}的函數，其包含以下五個主要轉換

(1)原子命題公式的語義解釋轉換；

(2)合取邏輯算子公式的語義解釋轉換；

(3)析取邏輯算子公式的語義解釋轉換；

(4)a算子公式的語義解釋轉換；