[發明專利]一種基于Coq的機器人控制系統時序安全性的驗證方法

有效

• 申請號: 202011390411.8
• 申請日: 2020-12-02
• 公開（公告）號: CN112463133B
• 公開（公告）日: 2022-06-10
• 發明（設計）人: 鄔惠峰;范寶文;孫潔香
• 申請（專利權）人: 杭州電子科技大學
• 主分類號: G06F8/30
• 分類號: G06F8/30;G06F8/35;G06F8/41;B25J9/16
• 代理公司: 浙江永鼎律師事務所 33233
• 代理人: 陸永強

本發明公開了基于Coq的機器人控制系統時序安全性的驗證方法，包括以下步驟：S10，抽象系統行為；S20，制定語義模型；S30，變量的形式化、轉移規則的形式化、期望性質的形式化和性質的驗證。本發明解決利用定理證明器驗證基于C語言的嵌入式系統時序安全性的問題。

技術領域

本發明屬于系統驗證技術領域，涉及一種基于Coq的機器人控制系統時序安全性的驗證方法。

背景技術

嵌入式系統廣泛地應用于各種生產場景中以輔助生產過程。機器人控制系統是一種典型的嵌入式系統的應用，而C語言被大量地應用于控制系統底層程序的開發。機器人的運動控制程序包含大量時序控制邏輯和硬件控制模塊，引入了C語言的時間處理模塊，增加了系統安全性驗證的難度。傳統測試方法的效果取決于測試用例的規模，其測試方法往往以函數為粒度，在復雜程序結構的情況下通常很難保證較好的測試覆蓋程度。因此對C語言編寫的控制軟件系統時序安全性的驗證是一個至今尚未有效解決的問題。

因此隨著嵌入式系統對安全性和高可靠性的要求不斷提高，形式化方法的應用顯得尤為重要。形式化方法主要分為模型檢測和定理證明兩種。前者利用驗證工具窮舉系統的狀態空間，能較好地驗證有窮程序。然而，模型檢測存在無法完成對復雜的數據類型和遞歸結構的推理及狀態爆炸問題，使得模型檢測只能處理控制為主、數據簡單的系統的程序，而無法對復雜系統的程序進行檢測。

Coq是一款交互式證明輔助工具，采用OCaml開發。Coq提供一套證明系統，可以編寫證明，檢查證明。Coq也提供一套形式化語言，可編寫數學算法、定義、定理。Coq也可以用于程序的正確性證明(比如操作系統的安全性和編譯器的正確性)。Coq作為一種被廣泛使用的定理證明器，其提供的描述形式化語言Gallina和交互式證明的開發環境可幫助使用者逐步推導形式化定理，或開發程序。此外Coq允許用戶自定義證明方法和策略語言，并使用外部的代數系統或定理證明器用于輔助證明。

發明內容

本發明提供一種基于Coq的機器人控制系統時序安全性的驗證方法，以解決利用定理證明器驗證基于C語言的嵌入式系統時序安全性的問題，并以三軸機器人為例進行驗證。

自動機是有限狀態機(FSM)的數學模型。Mealy自動機在FSM的基礎上增加了輸出，其次態是由輸入的變化和現態決定的。

本發明的技術方案為基于Coq的機器人控制系統時序安全性的驗證方法，包括以下步驟：

S10，抽象系統行為；

S20，制定語義模型；

S30，變量的形式化、轉移規則的形式化、期望性質的形式化和性質的驗證。

優選地，所述抽象系統行為，為依據機器人行為特征和C語言的特性，將系統的運行劃分為若干個階段，建立表示系統運行的自動機中間模型。將控制機器人運動的指令集抽象成離散的系統行為集合，作為自動機的輸入單詞的集合。

優選地，所述制定語義模型，為由自動機的狀態遷移寫出典型指令的操作語義，以統一抽象層次，解釋每條指令對系統格局的改變，形式化地規定轉移的規則。

優選地，所述變量的形式化、轉移規則的形式化、期望性質的形式化和性質的驗證，包括以下步驟：

S31，變量的形式化：確定中間件模型元素到Coq中類型的映射，使用Coq中的內建數據類型表示移動距離、全局時間變量；使用歸納類型定義系統的離散行為；使用全映射方式存儲系統臨時變量，定義變量相關的輔助函數；

S32，轉移規則的形式化：根據語義使用Coq的規范語言Gillina描述系統格局的轉移規則，建立系統的形式化模型，將定義的函數式轉換為命題的表現形式，便于性質的驗證；