穿刺機(jī)器人運(yùn)動(dòng)安全性的形式化分析與建模

孫浩然，施智平，3，關(guān) 永，王 瑞

1.首都師范大學(xué) 成像技術(shù)北京市高精尖創(chuàng)新中心，北京 100048

2.首都師范大學(xué) 信息工程學(xué)院 輕型工業(yè)機(jī)器人與安全驗(yàn)證北京市重點(diǎn)實(shí)驗(yàn)室，北京 100048

3.北京數(shù)學(xué)與信息交叉科學(xué)2011協(xié)同創(chuàng)新中心，北京 100048

1 引言

混成系統(tǒng)（hybrid system）[1-2]是一種嵌入在物理環(huán)境下的實(shí)時(shí)系統(tǒng)，一般由離散組件和連續(xù)組件連接組成，組件之間的行為由計(jì)算模型進(jìn)行控制。其中，連續(xù)組件一般通過(guò)系統(tǒng)變量對(duì)時(shí)間的微分方程來(lái)描述系統(tǒng)的實(shí)際控制模型以及系統(tǒng)中參數(shù)的演變規(guī)律；離散組件則通過(guò)狀態(tài)機(jī)、Petri網(wǎng)等高抽象層次的模型來(lái)描述系統(tǒng)的邏輯控制轉(zhuǎn)換過(guò)程。在兩個(gè)部分之間，通過(guò)一定的接口與規(guī)則將連續(xù)部分的信號(hào)與離散部分的控制模式進(jìn)行關(guān)聯(lián)與轉(zhuǎn)換。

隨著科技的發(fā)展，人們對(duì)控制系統(tǒng)行為的需求變得越來(lái)越復(fù)雜，使得混成系統(tǒng)在工業(yè)控制中大量出現(xiàn)。特別是在安全攸關(guān)的系統(tǒng)中，例如：醫(yī)療設(shè)施、航空航天、交通運(yùn)輸?shù)阮I(lǐng)域。同時(shí)，混成系統(tǒng)的失控所帶來(lái)的災(zāi)難也越來(lái)越沉重，例如飛機(jī)導(dǎo)航系統(tǒng)的失誤導(dǎo)致機(jī)毀人亡，芯片的設(shè)計(jì)錯(cuò)誤給公司帶來(lái)幾十億美元的回收代價(jià)，醫(yī)療設(shè)備突然失控奪去病人的寶貴生命等等。因此，對(duì)混成系統(tǒng)的安全性驗(yàn)證已經(jīng)成為一個(gè)亟待解決的問(wèn)題。

近幾十年來(lái)，形式化方法（formal method）[3-4]在很多領(lǐng)域中都取得了巨大進(jìn)步，基礎(chǔ)研究的進(jìn)展加上技術(shù)進(jìn)步的推動(dòng)，使新方法和新工具不斷出現(xiàn)并逐步完善成為一種成熟的高可靠驗(yàn)證技術(shù)。形式化方法是通過(guò)數(shù)學(xué)方法證明被驗(yàn)證系統(tǒng)滿(mǎn)足系統(tǒng)規(guī)范。根據(jù)數(shù)學(xué)理論來(lái)證明設(shè)計(jì)的系統(tǒng)是否滿(mǎn)足期望的性質(zhì)，在不能證明期望的性質(zhì)時(shí)，則可能發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤。形式化驗(yàn)證正是通過(guò)這種方式增強(qiáng)了對(duì)系統(tǒng)的理解和增加了發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤的機(jī)率。因此，本文將通過(guò)穿刺機(jī)器人的實(shí)例，使用形式化方法驗(yàn)證機(jī)器人運(yùn)動(dòng)控制系統(tǒng)的安全性。

形式化方法主要包括模型檢驗(yàn)（model checking）[5]和定理證明（theorem proving）[6]兩個(gè)方面。相較于模型檢驗(yàn)通過(guò)遍歷狀態(tài)空間來(lái)證明性質(zhì)的方法，定理證明主要采用邏輯和數(shù)學(xué)推理證明的方法驗(yàn)證關(guān)鍵性質(zhì)。針對(duì)狀態(tài)復(fù)雜的混成系統(tǒng)而言定理證明方法具有更良好的性能，并且已經(jīng)取得了一系列的進(jìn)展。

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

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

2 案例分析

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

2.1 穿刺機(jī)器人控制系統(tǒng)

穿刺機(jī)器人[14]是現(xiàn)代外科手術(shù)中較為普遍的技術(shù)，特別是在微創(chuàng)外科領(lǐng)域。當(dāng)前，穿刺術(shù)主要通過(guò)醫(yī)生手工完成，其準(zhǔn)確性和穿刺質(zhì)量完全依賴(lài)醫(yī)生的經(jīng)驗(yàn)和能力。近十年來(lái)，機(jī)器人輔助技術(shù)在現(xiàn)代醫(yī)學(xué)中的應(yīng)用得到越來(lái)越廣泛的認(rèn)可。以da Vinci，ZUES為代表的外科手術(shù)機(jī)器人系統(tǒng)在臨床上的成功案例吸引了醫(yī)學(xué)界、科技界極大的興趣。機(jī)器人輔助穿刺避免了醫(yī)生直接暴露在射線(xiàn)下，同時(shí)克服了醫(yī)生疲勞、手抖動(dòng)和手眼協(xié)調(diào)問(wèn)題等引起的操作誤差，提高了穿刺的精準(zhǔn)性和穩(wěn)定性。同時(shí)，穿刺機(jī)器人在醫(yī)療環(huán)境中的安全性、可控性等問(wèn)題也引起了人們的高度重視。

機(jī)器人輔助針穿刺系統(tǒng)主要有兩類(lèi)[15]：自主系統(tǒng)的安全性是本文討論的重點(diǎn)，因?yàn)樽灾飨到y(tǒng)是機(jī)器人輔助穿刺的最終目標(biāo)且面臨的安全性問(wèn)題更加嚴(yán)峻。穿刺針能否根據(jù)定位系統(tǒng)準(zhǔn)確地自主運(yùn)動(dòng)到靶點(diǎn)位置，能否在提高穿刺效率的同時(shí)保證安全性等等都是將要驗(yàn)證的問(wèn)題。本文不考慮機(jī)器人復(fù)雜的機(jī)構(gòu)學(xué)設(shè)計(jì)，僅從末端執(zhí)行器的運(yùn)動(dòng)學(xué)角度建模分析穿刺過(guò)程的安全性等問(wèn)題。

穿刺是外科手術(shù)中常見(jiàn)的手術(shù)動(dòng)作，可以根據(jù)操作環(huán)境和約束條件等因素將整體目標(biāo)分為四個(gè)子目標(biāo)，分別為加速運(yùn)動(dòng)（fast movement）、減速運(yùn)動(dòng)（slow movement）、垂直姿態(tài)（Perpendicular attitude）和穿刺（puncturing），如圖1所示。

圖1 穿刺運(yùn)動(dòng)過(guò)程

當(dāng)末端執(zhí)行器從初始狀態(tài)出發(fā)后為了盡快到達(dá)靶點(diǎn)位置開(kāi)始加速運(yùn)動(dòng)，在靶點(diǎn)附近到達(dá)某一制動(dòng)點(diǎn)位置時(shí)開(kāi)始減速運(yùn)動(dòng)，并最終在靶點(diǎn)位置處停止運(yùn)動(dòng)。之后調(diào)整穿刺針的姿態(tài)，當(dāng)穿刺針姿態(tài)與靶點(diǎn)所在表面方向垂直時(shí)進(jìn)行穿刺，到達(dá)終止?fàn)顟B(tài)時(shí)結(jié)束動(dòng)作。

本文將著重討論末端執(zhí)行器在任意初始狀態(tài)下以滿(mǎn)足約束的任意加速度開(kāi)始運(yùn)動(dòng)后，如何確定開(kāi)始制動(dòng)點(diǎn)的約束條件，保證末端執(zhí)行器以滿(mǎn)足約束的任意制動(dòng)力開(kāi)始減速并可以安全地停止在靶點(diǎn)位置。

2.2 微分動(dòng)態(tài)邏輯

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

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

混成系統(tǒng)可以用混成程序（hybrid programs）來(lái)進(jìn)行描述?；斐沙绦蚴且环N規(guī)范的應(yīng)用于混成系統(tǒng)形式化的模型?；斐沙绦蚩梢詫⒒斐上到y(tǒng)的離散跳轉(zhuǎn)和連續(xù)演化相結(jié)合，實(shí)現(xiàn)既簡(jiǎn)潔又準(zhǔn)確的形式化、結(jié)構(gòu)化的控制?；斐沙绦蛴扇齻€(gè)部分組成：離散跳變集、微分方程系統(tǒng)和控制結(jié)構(gòu)。離散跳變集包含了系統(tǒng)的離散變化，對(duì)狀態(tài)變量（實(shí)質(zhì)是微分方程中的變量）進(jìn)行瞬時(shí)的賦值操作。微分方程系統(tǒng)表示了動(dòng)態(tài)系統(tǒng)的連續(xù)性變化及其變化域?？刂平Y(jié)構(gòu)表示了離散和連續(xù)之間轉(zhuǎn)移的關(guān)系，利用操作符可以連接不同的混成程序，實(shí)現(xiàn)了系統(tǒng)間的聯(lián)系和交互。

下面是部分混成程序的表述形式以及對(duì)應(yīng)的作用效果。

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

（2）x′1=θ1,x′2=θ2,…,x′i=θi& χ：連續(xù)演化過(guò)程。由項(xiàng) θ1,θ2,…,θi組成的關(guān)于 x1,x2,…,xi的微分方程，并且?guī)в幸浑A邏輯的限制條件x1,x2,…,xi。

（3）狀態(tài)檢測(cè)。檢測(cè)當(dāng)前狀態(tài)的一階邏輯范式χ的值是否為真。

（4）α;β：順序組合。當(dāng)α完成后再順序執(zhí)行β。

（6）α＊：不確定性重復(fù)。重復(fù)執(zhí)行n次α，n可以是任意自然數(shù)。

2.3 形式化分析與驗(yàn)證

穿刺機(jī)器人的安全性指運(yùn)動(dòng)過(guò)程中，末端執(zhí)行器在滿(mǎn)足約束條件（區(qū)域限制，速度限制等）的前提下完成指定任務(wù)。

本文的目的是證明機(jī)器人部分穿刺過(guò)程的安全性。即，末端執(zhí)行器從安全區(qū)域出發(fā)，并在任何操作時(shí)間內(nèi)是安全的，且穿刺針到達(dá)靶目標(biāo)位置時(shí)速度滿(mǎn)足安全性限制。

如圖2所示，R1、R2分別表示機(jī)械臂可以執(zhí)行自由運(yùn)動(dòng)和減速運(yùn)動(dòng)的空間。Q1表示機(jī)械臂自由運(yùn)動(dòng)的終止平面，隨后機(jī)械臂進(jìn)入減速運(yùn)動(dòng)空間。Q2表示減速運(yùn)動(dòng)的終止平面，在穿刺針末端到達(dá)Q2平面時(shí)，穿刺針的速度與加速度均要滿(mǎn)足相應(yīng)的安全性約束，隨后調(diào)整穿刺針的穿刺姿態(tài)準(zhǔn)備穿刺。

圖2 穿刺運(yùn)動(dòng)空間模型

如果把穿刺過(guò)程的控制算法模型稱(chēng)為Ctrl，對(duì)于穿刺運(yùn)動(dòng)的整個(gè)控制過(guò)程，可以將其安全性質(zhì)描述為：

公式（2）中，蘊(yùn)含式前、后件中的safe表示安全區(qū)域，微分動(dòng)態(tài)邏輯算子[Ctrl]表示控制過(guò)程。因此上述蘊(yùn)含式表達(dá)了穿刺運(yùn)動(dòng)的末端執(zhí)行器從安全區(qū)域safe出發(fā)，通過(guò)[Ctrl]的控制后運(yùn)動(dòng)過(guò)程中的所有狀態(tài)依然保持在安全區(qū)域內(nèi)。

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

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

根據(jù)安全性描述，當(dāng)穿刺針到達(dá)m.pe時(shí)，速度滿(mǎn)足：

根據(jù)末端執(zhí)行器在空間上的運(yùn)動(dòng)方式本文將其分解為在z軸方向上一維微分動(dòng)態(tài)邏輯模型和在xoy平面上二維微分動(dòng)態(tài)邏輯模型。

3 一維微分動(dòng)態(tài)邏輯模型

末端執(zhí)行器在z軸方向上的運(yùn)動(dòng)方式如圖3所示。

圖3 Z軸方向上的運(yùn)動(dòng)學(xué)分析

圖3 中，sbp為開(kāi)始制動(dòng)點(diǎn)（Start braking point），m.pez為末端執(zhí)行器沿z軸運(yùn)動(dòng)的終點(diǎn)位置?？臻gR1和R2由邊界Q1隔開(kāi)。末端執(zhí)行器沿z軸運(yùn)動(dòng)的位置不能超出邊界Q2，即末端執(zhí)行器的位置始終滿(mǎn)足：

根據(jù)末端執(zhí)行器在z軸方向上的運(yùn)動(dòng)方式建立微分動(dòng)態(tài)邏輯子模型如下：

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

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

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

緊急制動(dòng)控制ebc的作用是在末端執(zhí)行器的位置δ.pz超過(guò)制動(dòng)點(diǎn)sbp或者控制臺(tái)向末端執(zhí)行器發(fā)出緊急制動(dòng)指令command:=brake時(shí)以末端執(zhí)行器允許達(dá)到的最大制動(dòng)力開(kāi)始制動(dòng)。

控制臺(tái)Console表示給出緊急制動(dòng)指令command:=brake或者將末端執(zhí)行器的約束值修改為任意值。例如：由于實(shí)際情況中靶點(diǎn)目標(biāo)的移動(dòng)從而將目標(biāo)位置的取值m.pez修改為移動(dòng)后的值。

3.1 歸納微分不變式

根據(jù)安全性要求，末端執(zhí)行器在運(yùn)動(dòng)到終點(diǎn)位置m.pez時(shí)不會(huì)超過(guò)限制速度m.vez，用微分動(dòng)態(tài)邏輯公式描述為：

根據(jù)動(dòng)力學(xué)系統(tǒng)要求，可以得到全局性的約束條件：

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

根據(jù)以上分析可以得到動(dòng)力學(xué)系統(tǒng)可控性約束的微分動(dòng)態(tài)邏輯方程，令：

則

上述方程表示當(dāng)末端執(zhí)行器從滿(mǎn)足全局性約束條件且沒(méi)有通過(guò)終點(diǎn)m.pez的狀態(tài)下出發(fā)，對(duì)于所有的連續(xù)演化過(guò)程，末端執(zhí)行器以最大的制動(dòng)力m.Min執(zhí)行減速運(yùn)動(dòng)的狀態(tài)都滿(mǎn)足安全性約束δ.pz≥m.pez→δ.vz≤m.vez。

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

則

在實(shí)際操作情況中，需要考慮到特殊情況，例如末端執(zhí)行器從一開(kāi)始就以最大加速度加速運(yùn)動(dòng)，在到達(dá)制動(dòng)點(diǎn)sbpz后開(kāi)始減速運(yùn)動(dòng)并最終安全到達(dá)終點(diǎn)位置m.pez。用微分動(dòng)態(tài)邏輯公式描述為：

上述公式表示末端執(zhí)行器從安全狀態(tài)集出發(fā)并且以最大加速度δ.v′z=m.Max運(yùn)行后仍在安全狀態(tài)集中。又因?yàn)榘踩珷顟B(tài)集Inv表示末端執(zhí)行器無(wú)論以什么樣的速度運(yùn)動(dòng)，之后以最大的制動(dòng)力m.Min制動(dòng)都可以滿(mǎn)足終點(diǎn)位置的速度限制。使用證明工具KeYmaera對(duì)上述微分動(dòng)態(tài)邏輯公式進(jìn)行推理證明，得到：

由上式得出了開(kāi)始制動(dòng)點(diǎn)sbpz位置的約束解。

3.2 參數(shù)可變的微分動(dòng)態(tài)邏輯模型

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

由于不變式Inv是過(guò)程性約束，它更深層的含義是指當(dāng)末端執(zhí)行器目前的狀態(tài)滿(mǎn)足安全性約束則它之后的某個(gè)狀態(tài)若滿(mǎn)足不變式Inv的約束也必定滿(mǎn)足安全性約束。因此，當(dāng)目前的參數(shù)滿(mǎn)足安全性約束，經(jīng)Console更改后若仍然滿(mǎn)足不變式Inv的約束，則更改后的參數(shù)也一定滿(mǎn)足安全性約束，即

本文通過(guò)推理證明的方法分析說(shuō)明在末端執(zhí)行器的運(yùn)動(dòng)過(guò)程中更改約束參數(shù)的安全性，有以下微分動(dòng)態(tài)邏輯公式：

上述公式表示末端執(zhí)行器從滿(mǎn)足不變式Inv的狀態(tài)下出發(fā)，對(duì)于所有的約束參數(shù)的更改[m:=m′]，如果更改后的狀態(tài)滿(mǎn)足UpdateInv則所有的狀態(tài)滿(mǎn)足可控性約束。即

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

由于本文將末端執(zhí)行器在空間上的運(yùn)動(dòng)方式分解為兩部分，在以上一維空間運(yùn)動(dòng)控制模型的基礎(chǔ)上，本文將進(jìn)一步分析機(jī)器人在二維空間中的運(yùn)動(dòng)情況并建立二維微分動(dòng)態(tài)邏輯模型。

4 二維微分動(dòng)態(tài)邏輯模型

如圖4所示，A和B為同心圓。區(qū)域A為執(zhí)行穿刺的目標(biāo)區(qū)域，區(qū)域B為末端執(zhí)行器能夠安全到達(dá)區(qū)域A的減速區(qū)域。區(qū)域A和B以外的區(qū)域?yàn)樽杂蛇\(yùn)動(dòng)區(qū)域。A1和B1分別為A和B的邊界；a、b分別為直線(xiàn)b1、b2與圓A的切點(diǎn)，且b1||b2。坐標(biāo)系的原點(diǎn)O為末端執(zhí)行器的啟動(dòng)位置。vx、vy表示末端執(zhí)行器在x和y方向上的分速度。d和D分別為圓A和B的半徑大小。

圖4 xOy平面上的運(yùn)動(dòng)學(xué)分析

實(shí)際中，根據(jù)末端執(zhí)行器的位置與靶點(diǎn)位置的關(guān)系可以分為以下兩種情況：

（1）δ.pxy-Ao≥D，表示末端執(zhí)行器處于可自由運(yùn)動(dòng)的區(qū)域。在該區(qū)域中，末端執(zhí)行器可以以任意速度vx、vy運(yùn)動(dòng)，其中，0≤vx≤m.vm，0≤vy≤m.vm。當(dāng)末端執(zhí)行器到達(dá)邊界B1時(shí)執(zhí)行減速運(yùn)動(dòng)。

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

經(jīng)過(guò)圓心Ao（Ao即終點(diǎn)m.pe在xOy平面上的投影位置）的兩條直線(xiàn)a1、a2為末端執(zhí)行器終止運(yùn)動(dòng)的邊界，即末端執(zhí)行器在x和y方向上分別逼近a1、a2，但始終不會(huì)越過(guò)a1、a2。

由于末端執(zhí)行器在xOy平面上的運(yùn)動(dòng)是自由的，分析可知spd=D，即假設(shè)Ao為最理想的靶點(diǎn)位置，D為滿(mǎn)足約束性條件的最小的制動(dòng)距離。在實(shí)際的醫(yī)療環(huán)境中醫(yī)生不會(huì)允許穿刺針無(wú)終止地運(yùn)動(dòng)，為了保證執(zhí)行動(dòng)作的高效性，本文假設(shè)末端執(zhí)行器必須在b1和b2之間的區(qū)域內(nèi)運(yùn)動(dòng)，即犧牲運(yùn)動(dòng)的部分靈活性實(shí)現(xiàn)高效性。在這個(gè)區(qū)域內(nèi)末端執(zhí)行器可以在滿(mǎn)足約束條件的情況下自由運(yùn)動(dòng)。

4.1 xOy平面上的運(yùn)動(dòng)學(xué)模型

根據(jù)末端執(zhí)行器在xOy平面上的運(yùn)動(dòng)方式建立微分動(dòng)態(tài)邏輯子模型如下：

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

圖5 迭代延時(shí)分析

4.2 運(yùn)動(dòng)學(xué)問(wèn)題的一般性驗(yàn)證模型

圖6 安全運(yùn)動(dòng)的一般性形式化模型

因此當(dāng)末端執(zhí)行器在y軸方向上運(yùn)動(dòng)的終點(diǎn)位置由Ao變?yōu)榻私K止點(diǎn)A.a3時(shí)，m.pey:=Ao-d。同理，終點(diǎn)位置變?yōu)檫h(yuǎn)端終止點(diǎn)A.a4時(shí)，m.pey:=Ao+d，所以sbpy:=(Ao±d)-δ.py。因此，在 y軸方向上若要滿(mǎn)足末端執(zhí)行器最終停在圓A內(nèi)y軸方向上的任意位置時(shí)，開(kāi)始制動(dòng)點(diǎn)的取值范圍為：

假設(shè)末端執(zhí)行器停止在圓A內(nèi)e點(diǎn)處，則在x軸方向上的約束邊界由b1、b2變?yōu)閎3、b4。開(kāi)始制動(dòng)點(diǎn)到邊界b3、b4的垂直距離為為末端執(zhí)行器在y軸上的停止位置。因此：

綜上所述，得到末端執(zhí)行器在xOy軸方向上的運(yùn)動(dòng)方式建立微分動(dòng)態(tài)邏輯子模型如下：

從運(yùn)動(dòng)學(xué)角度分析，以上微分動(dòng)態(tài)邏輯模型對(duì)于機(jī)器人到達(dá)某一指定區(qū)域的安全性問(wèn)題具有普適性約束，可以作為空間運(yùn)動(dòng)學(xué)安全性問(wèn)題的一般性驗(yàn)證模型。若末端執(zhí)行器要求準(zhǔn)確到達(dá)某一點(diǎn)，則可犧牲部分靈活性，保證運(yùn)動(dòng)的安全性。如圖6（b）所示，可以以靶點(diǎn)為頂點(diǎn)做錐形空間，則末端執(zhí)行器在x軸方向上約束條件為：

為了證明用微分動(dòng)態(tài)邏輯描述的混成系統(tǒng)的安全性，本文結(jié)合機(jī)器人控制系統(tǒng)的安全性描述，將以上微分動(dòng)態(tài)邏輯模型Ctrl4寫(xiě)入后綴名為key的文件后，導(dǎo)入KeYmaera中進(jìn)行自動(dòng)推理證明。在KeYmaera自動(dòng)證明的過(guò)程中，為了加快驗(yàn)證進(jìn)度，人為地加入了一些驗(yàn)證過(guò)程中必要的邏輯法則。最終KeYmaera彈出“property proved”，證明了模型的安全性。

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

本文通過(guò)微分動(dòng)態(tài)邏輯的方法對(duì)穿刺機(jī)器人自主系統(tǒng)部分安全性問(wèn)題進(jìn)行了驗(yàn)證。從運(yùn)動(dòng)描述中提取出形式化模型，通過(guò)推理規(guī)則精化出滿(mǎn)足系統(tǒng)安全性要求的微分不變式及系統(tǒng)約束參數(shù)可變的安全性證明。此外，本文從穿刺機(jī)器人的實(shí)例出發(fā)提出了一種可以證明空間運(yùn)動(dòng)學(xué)安全性問(wèn)題的一般性形式化模型，該模型能夠適用于與本文工作相似的空間運(yùn)動(dòng)學(xué)設(shè)計(jì)問(wèn)題。