穿刺機器人運動安全性的形式化分析與建模

孫浩然，施智平，3，關 永，王 瑞

1.首都師范大學 成像技術北京市高精尖創新中心，北京 100048

2.首都師范大學 信息工程學院 輕型工業機器人與安全驗證北京市重點實驗室，北京 100048

3.北京數學與信息交叉科學2011協同創新中心，北京 100048

1 引言

混成系統（hybrid system）[1-2]是一種嵌入在物理環境下的實時系統，一般由離散組件和連續組件連接組成，組件之間的行為由計算模型進行控制。其中，連續組件一般通過系統變量對時間的微分方程來描述系統的實際控制模型以及系統中參數的演變規律；離散組件則通過狀態機、Petri網等高抽象層次的模型來描述系統的邏輯控制轉換過程。在兩個部分之間，通過一定的接口與規則將連續部分的信號與離散部分的控制模式進行關聯與轉換。

隨著科技的發展，人們對控制系統行為的需求變得越來越復雜，使得混成系統在工業控制中大量出現。特別是在安全攸關的系統中，例如：醫療設施、航空航天、交通運輸等領域。同時，混成系統的失控所帶來的災難也越來越沉重，例如飛機導航系統的失誤導致機毀人亡，芯片的設計錯誤給公司帶來幾十億美元的回收代價，醫療設備突然失控奪去病人的寶貴生命等等。因此，對混成系統的安全性驗證已經成為一個亟待解決的問題。

近幾十年來，形式化方法（formal method）[3-4]在很多領域中都取得了巨大進步，基礎研究的進展加上技術進步的推動，使新方法和新工具不斷出現并逐步完善成為一種成熟的高可靠驗證技術。形式化方法是通過數學方法證明被驗證系統滿足系統規范。根據數學理論來證明設計的系統是否滿足期望的性質，在不能證明期望的性質時，則可能發現設計錯誤。形式化驗證正是通過這種方式增強了對系統的理解和增加了發現設計錯誤的機率。因此，本文將通過穿刺機器人的實例，使用形式化方法驗證機器人運動控制系統的安全性。

形式化方法主要包括模型檢驗（model checking）[5]和定理證明（theorem proving）[6]兩個方面。相較于模型檢驗通過遍歷狀態空間來證明性質的方法，定理證明主要采用邏輯和數學推理證明的方法驗證關鍵性質。針對狀態復雜的混成系統而言定理證明方法具有更良好的性能，并且已經取得了一系列的進展。

何積豐院士等人在CSP[7]基礎上提出了混成CSP語言，可以用來描述組合混成系統。Sankaranarayana等人提出了生成混成系統不變式的方法[8]，該方法利用約束求解的方法預先給出多項式模板，然后基于模板生成多項式不變式；詹乃軍老師等人提出了一種通過李導數求解混成系統半代數不變式的方法[9]。此外，Barrier Certificate[10]是混成系統不變式生成方向上的又一個重要成果，Prajna提出了一種通過利用平方和（sum of square）與半定規劃（semidefinite programming）技術來生成多項式不等式形式的混成自動機不變式的方法。

與以上方法相比，本文采用微分動態邏輯（differential dynamic logic）[11]的方法驗證穿刺機器人的安全性，該方法被視為近期混成系統定理證明領域的重大突破。微分動態邏輯主要思想是：不求解微分方程，而是尋找這些微分方程的微分不變式（differential invariant）[12]，從而避免了求解微分方程可能導致的不可控計算量問題。

2 案例分析

機器人輔助醫療技術[13]是現代外科醫學的重要研究方向。研究機器人輔助穿刺技術的安全性不僅具有重要的理論價值，而且在臨床上可以有效地提高穿刺的安全性和活性。

2.1 穿刺機器人控制系統

穿刺機器人[14]是現代外科手術中較為普遍的技術，特別是在微創外科領域。當前，穿刺術主要通過醫生手工完成，其準確性和穿刺質量完全依賴醫生的經驗和能力。近十年來，機器人輔助技術在現代醫學中的應用得到越來越廣泛的認可。以da Vinci，ZUES為代表的外科手術機器人系統在臨床上的成功案例吸引了醫學界、科技界極大的興趣。機器人輔助穿刺避免了醫生直接暴露在射線下，同時克服了醫生疲勞、手抖動和手眼協調問題等引起的操作誤差，提高了穿刺的精準性和穩定性。同時，穿刺機器人在醫療環境中的安全性、可控性等問題也引起了人們的高度重視。

機器人輔助針穿刺系統主要有兩類[15]：自主系統的安全性是本文討論的重點，因為自主系統是機器人輔助穿刺的最終目標且面臨的安全性問題更加嚴峻。穿刺針能否根據定位系統準確地自主運動到靶點位置，能否在提高穿刺效率的同時保證安全性等等都是將要驗證的問題。本文不考慮機器人復雜的機構學設計，僅從末端執行器的運動學角度建模分析穿刺過程的安全性等問題。

穿刺是外科手術中常見的手術動作，可以根據操作環境和約束條件等因素將整體目標分為四個子目標，分別為加速運動（fast movement）、減速運動（slow movement）、垂直姿態（Perpendicular attitude）和穿刺（puncturing），如圖1所示。

圖1 穿刺運動過程

當末端執行器從初始狀態出發后為了盡快到達靶點位置開始加速運動，在靶點附近到達某一制動點位置時開始減速運動，并最終在靶點位置處停止運動。之后調整穿刺針的姿態，當穿刺針姿態與靶點所在表面方向垂直時進行穿刺，到達終止狀態時結束動作。

本文將著重討論末端執行器在任意初始狀態下以滿足約束的任意加速度開始運動后，如何確定開始制動點的約束條件，保證末端執行器以滿足約束的任意制動力開始減速并可以安全地停止在靶點位置。

2.2 微分動態邏輯

微分動態邏輯是建立在混成系統上的一階邏輯，具有描述混成系統性質的能力，可以簡潔地表達出混成系統的安全性等性質。微分動態系統的原理是在單個的形式化語言中將系統的操作及系統正確的狀態聲明結合在一起。允許系統操作α作為模態邏輯的動作，為動態邏輯提供形如[α]? 和 <α＞? 的公式。[α]? 表示系統α的所有運行狀態均滿足條件?；<α＞?表示在系統α的所有運行狀態中至少存在這樣一個狀態滿足條件?。在微分動態邏輯中，混成程序（hybrid programs）通常扮演α的角色。

微分動態邏輯具有詳細的推理證明演算法則，實質上是一種便于證明的標準邏輯公式。一般公式形如，前提條件為Γ，而結論為Δ。此公式的語義等同于證明演算是一種推理規則，可以推理出公式正確或錯誤的性質。微分動態邏輯規則是基于一階邏輯規則的擴展，加入了針對量詞消去、微分方程的替換規則，由于混合了的運算，需要消去這些運算從而轉化為基本的一階邏輯公式。例如公式（1）自底向上表述了離散過程中可以表示為在公式?中將 xn替換成θn，從而消去了算子。

混成系統可以用混成程序（hybrid programs）來進行描述。混成程序是一種規范的應用于混成系統形式化的模型。混成程序可以將混成系統的離散跳轉和連續演化相結合，實現既簡潔又準確的形式化、結構化的控制。混成程序由三個部分組成：離散跳變集、微分方程系統和控制結構。離散跳變集包含了系統的離散變化，對狀態變量（實質是微分方程中的變量）進行瞬時的賦值操作。微分方程系統表示了動態系統的連續性變化及其變化域。控制結構表示了離散和連續之間轉移的關系，利用操作符可以連接不同的混成程序，實現了系統間的聯系和交互。

下面是部分混成程序的表述形式以及對應的作用效果。

（1）x1:θ1,x2:θ2,…,xi:θi：離散的跳變集，同時將值θ1,θ2,…,θi分別賦值給 x1,x2,…,xi。

（2）x′1=θ1,x′2=θ2,…,x′i=θi& χ：連續演化過程。由項 θ1,θ2,…,θi組成的關于 x1,x2,…,xi的微分方程，并且帶有一階邏輯的限制條件x1,x2,…,xi。

（3）狀態檢測。檢測當前狀態的一階邏輯范式χ的值是否為真。

（4）α;β：順序組合。當α完成后再順序執行β。

（6）α＊：不確定性重復。重復執行n次α，n可以是任意自然數。

2.3 形式化分析與驗證

穿刺機器人的安全性指運動過程中，末端執行器在滿足約束條件（區域限制，速度限制等）的前提下完成指定任務。

本文的目的是證明機器人部分穿刺過程的安全性。即，末端執行器從安全區域出發，并在任何操作時間內是安全的，且穿刺針到達靶目標位置時速度滿足安全性限制。

如圖2所示，R1、R2分別表示機械臂可以執行自由運動和減速運動的空間。Q1表示機械臂自由運動的終止平面，隨后機械臂進入減速運動空間。Q2表示減速運動的終止平面，在穿刺針末端到達Q2平面時，穿刺針的速度與加速度均要滿足相應的安全性約束，隨后調整穿刺針的穿刺姿態準備穿刺。

圖2 穿刺運動空間模型

如果把穿刺過程的控制算法模型稱為Ctrl，對于穿刺運動的整個控制過程，可以將其安全性質描述為：

公式（2）中，蘊含式前、后件中的safe表示安全區域，微分動態邏輯算子[Ctrl]表示控制過程。因此上述蘊含式表達了穿刺運動的末端執行器從安全區域safe出發，通過[Ctrl]的控制后運動過程中的所有狀態依然保持在安全區域內。

假設機械臂的末端執行器用δ=(p,v,a)表示在當前位置δ.p時具有速度δ.v和加速度δ.a，顯然有：

假設用五元組m=(pe,ve,vm,Max,Min)給出機械臂在運動過程中的某些約束概念。機械臂在運動過程中到達位于Q2平面上的終點m.pe（end point）時速度不大于m.ve，機械臂在運動過程中的速度不允許超過最大速度m.vm（max speed），m.Max與m.Min分別表示末端執行器的加速度在實際情況中的安全性限制，即-m.Min≤δ.a≤m.Max。

根據安全性描述，當穿刺針到達m.pe時，速度滿足：

根據末端執行器在空間上的運動方式本文將其分解為在z軸方向上一維微分動態邏輯模型和在xoy平面上二維微分動態邏輯模型。

3 一維微分動態邏輯模型

末端執行器在z軸方向上的運動方式如圖3所示。

圖3 Z軸方向上的運動學分析

圖3 中，sbp為開始制動點（Start braking point），m.pez為末端執行器沿z軸運動的終點位置。空間R1和R2由邊界Q1隔開。末端執行器沿z軸運動的位置不能超出邊界Q2，即末端執行器的位置始終滿足：

根據末端執行器在z軸方向上的運動方式建立微分動態邏輯子模型如下：

CTRL1表示末端執行器的運動控制由Move和Console兩部分組成。Move由運動學微分方程run（kinematic differential equation）、速度控制 sc（speed control）和緊急制動控制 ebc（emergency braking control）三部分組成。δ.pz′給出了末端執行器的位置δ.pz的變化速率，即δ.vz，而δ.vz的變化率對應相應的加速度δ.az，當 0<δ.az≤m.Max 時末端執行器加速運動，當-m.Min<δ.az<0時末端執行器減速運動。

在實際情況中，由于在z軸方向上末端執行器的運動方向始終指向邊界Q2，不存在相反方向的運動，所以用δ.vz≥0約束動力學微分方程。另外，末端執行器的速度不允許超過最大速度，即δ.vz≤m.vm。當該運動系統由離散跳轉轉到連續演化時，在連續演化開始之前將時間置零，即t:=0。因為該運動系統在實際中并非是理想的，所以會由硬件上的缺陷、通信的延遲等引入誤差，導致連續演化并不能立即得到響應，因此假設在t≤ε（ε＞0）內連續演化繼續執行則認為控制策略生效。

速度控制sc由兩個部分組成，符號?表示非確定性選擇。若判斷（符號?表示判斷）末端執行器的速度δ.vz不大于最大速度m.vm為真，則加速度δ.az可以在[-m.Min,m.Max]中任意取值，即末端執行器自由運動；若判斷δ.vz≥m.vm為真，則δ.az在[-m.Min,0]之間取值，使得末端執行器減速運動以保證運動速度不會超出控制。

緊急制動控制ebc的作用是在末端執行器的位置δ.pz超過制動點sbp或者控制臺向末端執行器發出緊急制動指令command:=brake時以末端執行器允許達到的最大制動力開始制動。

控制臺Console表示給出緊急制動指令command:=brake或者將末端執行器的約束值修改為任意值。例如：由于實際情況中靶點目標的移動從而將目標位置的取值m.pez修改為移動后的值。

3.1 歸納微分不變式

根據安全性要求，末端執行器在運動到終點位置m.pez時不會超過限制速度m.vez，用微分動態邏輯公式描述為：

根據動力學系統要求，可以得到全局性的約束條件：

由于在z軸方向上，末端執行器到達終點位置m.pez(δ.pz≤m.pez)以前，其運動方向始終指向邊界Q2，不存在反方向的運動過程，所以末端執行器的運動速度始終為非負值（δ.vz≥0）。末端執行器在z軸方向上的運動速度始終不會超過最大限速m.vm(δ.vz≤m.vm)。制動力m.Min＞0確保末端執行器可以做減速運動，加速度m.Max≥0確保末端執行器可以做加速或勻速運動。

根據以上分析可以得到動力學系統可控性約束的微分動態邏輯方程，令：

則

上述方程表示當末端執行器從滿足全局性約束條件且沒有通過終點m.pez的狀態下出發，對于所有的連續演化過程，末端執行器以最大的制動力m.Min執行減速運動的狀態都滿足安全性約束δ.pz≥m.pez→δ.vz≤m.vez。

使用證明工具KeYmaera對上述公式推理證明得到，當初始狀態滿足δ.vz2-m.vez2≤2m.Min(m.pez-δ.pz)時，上述微分動態邏輯公式成立，即δ.vz2-m.vez2≤2m.Min(m.pez-δ.pz)表示在滿足全局性約束條件下末端執行器以最大的制動力m.Min執行減速運動的狀態都滿足安全性約束，稱該式為系統的一個微分不變式（differential invariant）。結合全局性約束條件可以得到系統的全局性初始約束條件Inv，該條件滿足制動后的安全性約束，令：

則

在實際操作情況中，需要考慮到特殊情況，例如末端執行器從一開始就以最大加速度加速運動，在到達制動點sbpz后開始減速運動并最終安全到達終點位置m.pez。用微分動態邏輯公式描述為：

上述公式表示末端執行器從安全狀態集出發并且以最大加速度δ.v′z=m.Max運行后仍在安全狀態集中。又因為安全狀態集Inv表示末端執行器無論以什么樣的速度運動，之后以最大的制動力m.Min制動都可以滿足終點位置的速度限制。使用證明工具KeYmaera對上述微分動態邏輯公式進行推理證明，得到：

由上式得出了開始制動點sbpz位置的約束解。

3.2 參數可變的微分動態邏輯模型

由于在實際的醫療環境中存在諸多不可控因素，導致需要及時更改末端執行器的約束參數或靶點位置等信息，使得穿刺機器人仍然可以繼續正確執行穿刺動作。例如：醫生根據手術過程中的實際情況需要盡快完成穿刺動作而提高末端執行器的最大運動速度m.vm或最大加速度m.Max的取值；又或者，由于手術過程中靶點位置的移動需要及時更改靶點位置m.pe的取值等。對于上述情況控制臺Console將及時更新m=(pe,ve,vm,Max,Min)的值為 m′。

由于不變式Inv是過程性約束，它更深層的含義是指當末端執行器目前的狀態滿足安全性約束則它之后的某個狀態若滿足不變式Inv的約束也必定滿足安全性約束。因此，當目前的參數滿足安全性約束，經Console更改后若仍然滿足不變式Inv的約束，則更改后的參數也一定滿足安全性約束，即

本文通過推理證明的方法分析說明在末端執行器的運動過程中更改約束參數的安全性，有以下微分動態邏輯公式：

上述公式表示末端執行器從滿足不變式Inv的狀態下出發，對于所有的約束參數的更改[m:=m′]，如果更改后的狀態滿足UpdateInv則所有的狀態滿足可控性約束。即

開始制動點sbp的取值是在最嚴格的條件下計算得到的，即在制動點前以最大的加速度m.Max加速運動，到達制動點以后以最大制動力m.Min做減速運動，且到達終點位置m.pez時滿足最終的速度約束δ.vz≤m.vez。因此，當緊急制動控制ebc滿足m.pez-δ.pz≤sbp時開始緊急制動，穿刺機器人的末端執行器在z軸方向上的運動一定滿足安全性約束。

由于本文將末端執行器在空間上的運動方式分解為兩部分，在以上一維空間運動控制模型的基礎上，本文將進一步分析機器人在二維空間中的運動情況并建立二維微分動態邏輯模型。

4 二維微分動態邏輯模型

如圖4所示，A和B為同心圓。區域A為執行穿刺的目標區域，區域B為末端執行器能夠安全到達區域A的減速區域。區域A和B以外的區域為自由運動區域。A1和B1分別為A和B的邊界；a、b分別為直線b1、b2與圓A的切點，且b1||b2。坐標系的原點O為末端執行器的啟動位置。vx、vy表示末端執行器在x和y方向上的分速度。d和D分別為圓A和B的半徑大小。

圖4 xOy平面上的運動學分析

實際中，根據末端執行器的位置與靶點位置的關系可以分為以下兩種情況：

（1）δ.pxy-Ao≥D，表示末端執行器處于可自由運動的區域。在該區域中，末端執行器可以以任意速度vx、vy運動，其中，0≤vx≤m.vm，0≤vy≤m.vm。當末端執行器到達邊界B1時執行減速運動。

（2）d≤δ.pxy-Ao≤D，表示末端執行器處于邊界A1與B1之間的減速區域之中。

經過圓心Ao（Ao即終點m.pe在xOy平面上的投影位置）的兩條直線a1、a2為末端執行器終止運動的邊界，即末端執行器在x和y方向上分別逼近a1、a2，但始終不會越過a1、a2。

由于末端執行器在xOy平面上的運動是自由的，分析可知spd=D，即假設Ao為最理想的靶點位置，D為滿足約束性條件的最小的制動距離。在實際的醫療環境中醫生不會允許穿刺針無終止地運動，為了保證執行動作的高效性，本文假設末端執行器必須在b1和b2之間的區域內運動，即犧牲運動的部分靈活性實現高效性。在這個區域內末端執行器可以在滿足約束條件的情況下自由運動。

4.1 xOy平面上的運動學模型

根據末端執行器在xOy平面上的運動方式建立微分動態邏輯子模型如下：

但由于在速度迭代似的反饋控制中存在延時，假設延時時間為ε。如圖5所示，當傳感器將末端執行器當前的位置pxn反饋給Console并由它更改末端執行器在x軸方向上的速度時，執行器的位置已到達δ.px(n+1)=δ.pxn+vxn?ε之后執行更改后的速度vx(n+1)，此時可以保證末端執行器在速度迭代控制過程中存在延時ε的情況下依然不會超出約束邊界。

圖5 迭代延時分析

4.2 運動學問題的一般性驗證模型

圖6 安全運動的一般性形式化模型

因此當末端執行器在y軸方向上運動的終點位置由Ao變為近端終止點A.a3時，m.pey:=Ao-d。同理，終點位置變為遠端終止點A.a4時，m.pey:=Ao+d，所以sbpy:=(Ao±d)-δ.py。因此，在 y軸方向上若要滿足末端執行器最終停在圓A內y軸方向上的任意位置時，開始制動點的取值范圍為：

假設末端執行器停止在圓A內e點處，則在x軸方向上的約束邊界由b1、b2變為b3、b4。開始制動點到邊界b3、b4的垂直距離為為末端執行器在y軸上的停止位置。因此：

綜上所述，得到末端執行器在xOy軸方向上的運動方式建立微分動態邏輯子模型如下：

從運動學角度分析，以上微分動態邏輯模型對于機器人到達某一指定區域的安全性問題具有普適性約束，可以作為空間運動學安全性問題的一般性驗證模型。若末端執行器要求準確到達某一點，則可犧牲部分靈活性，保證運動的安全性。如圖6（b）所示，可以以靶點為頂點做錐形空間，則末端執行器在x軸方向上約束條件為：

為了證明用微分動態邏輯描述的混成系統的安全性，本文結合機器人控制系統的安全性描述，將以上微分動態邏輯模型Ctrl4寫入后綴名為key的文件后，導入KeYmaera中進行自動推理證明。在KeYmaera自動證明的過程中，為了加快驗證進度，人為地加入了一些驗證過程中必要的邏輯法則。最終KeYmaera彈出“property proved”，證明了模型的安全性。

5 結束語

本文通過微分動態邏輯的方法對穿刺機器人自主系統部分安全性問題進行了驗證。從運動描述中提取出形式化模型，通過推理規則精化出滿足系統安全性要求的微分不變式及系統約束參數可變的安全性證明。此外，本文從穿刺機器人的實例出發提出了一種可以證明空間運動學安全性問題的一般性形式化模型，該模型能夠適用于與本文工作相似的空間運動學設計問題。