2018年領域模型與形式化驗證技術.pdf

《2018年領域模型與形式化驗證技術.pdf》由會員分享，可在線閱讀，更多相關《2018年領域模型與形式化驗證技術.pdf（60頁珍藏版）》請在三個皮匠報告上搜索。

1、領域模型與形式化驗證技術領域模型與形式化驗證技術 中興通訊操作系統 李凱航 CONTENTS 01 形式化技術簡介 1.1 定理證明 1.2 模型檢測 1.3 LTL概念 02 怎樣驗證領域模型的正確性 2.1 用時態邏輯狀態機表達模型 2.2 用不變式檢查模型歸納性質 2.3 用線性時態邏輯檢查模型正確性 2.4 Intel ACRN InterruptWindow模型正確性驗證 03 怎樣用形式化技術推導一個正確模型 3.1 理論方法 3.2 物聯網操作系統內存管理模型設計推導 軟件正確性如何保證？大家知道的方法 編碼測試需求模型分析模型設計模型同行評審同行評審代碼走查需求模型編碼TDD用

2、例重構修正大家知道的方法 問題一：需求如何建模？圖、表、語言、文字等更加感性的東西，能否表達清楚用戶到底需要什么？問題二：需求分析到領域模型的正確性如何驗證？傳統的同行評審存在較大程度人為經驗的因素，包括評審組人員的構成、背景、經驗都會最終影響設計正確性的保證。需求實例化領域模型編碼驗收測試TDDDSL(BDD)修正修正我們的方法是什么我們的方法是什么 領域模型需求模型數學形式化模型數學形式化驗證定理模型：代碼模型領域模型需求模型數學形式化模型模型驗證定理模型時態邏輯狀態機模型不變式+時態屬性求精形式化技術簡介 形式化技術簡介 由于傳統的軟件工程方法無法從根本上保證軟件設計的安全性、正確性，因

3、此必須有一種客觀性的理論方法來保證在需求分析、概念建模階段就存在一個可量化、能夠驗證的模型才能從根本上解決上述問題，這種方法在目前業界叫做形式化方法，形式化方法的核心就是形式化語言，以及基于形式化語言構建出來的形式化模型。定理證明模型檢測定理證明 基本原理是使用數理邏輯公式規格化描述目標系統模型、需要滿足的性質，使用數理邏輯的公理、定理、推導規則結合系統模型的描述公式推導出系統需要滿足的性質。系統模型定理推導系統性質模型正確X需要人工干預？X模型檢測 將系統建模成有限狀態系統，系統的性質用時態邏輯公式表示如：CTL，LTL等，在此模型上利用狀態窮舉計算來驗證性質的正確性，模型檢測與定理證明相比

4、有很大優勢，可以全自動地驗證，不需要人工干預，而定理證明則在一些關鍵推導路徑中需要數學家控制，但是模型檢測有可能會產生狀態組合爆炸。系統模型系統性質全自動模型狀態窮舉計算模型正確XX狀態組合爆炸？LTLLTL概念 線性時態邏輯是由命題時態邏輯（PTL）和一階時態邏輯（FOTL）組成，其中PTL、FOTL本質上是在命題邏輯、一階邏輯基礎上擴展了模態詞或時態算子的模態邏輯。always算子 -F表示F總是為真或者F永遠為真 sometimes算子 -F表示F最終為真或者F有時為真 next算子 -F表示F在下一時刻為真 until算子 -F1 F2表示F1一直為真直到F2為真 線性時態邏輯所用到的

5、時態算子 LTLLTL概念 命題時態邏輯公式的BNF表示為：:=P|一階時態邏輯公式的BNF表示為：:=P|x.|x.|PTL公式和FOTL公式統稱為LTL公式 怎樣驗證領域模型的正確性 用時態邏輯狀態機表達領域模型 一個現實中的例子：VT01用時態邏輯狀態機表達領域模型 波形的變換符合下面規律：v=0-v=1-v=0-v=1.這是一個有規律變化的無窮序列 給了我們一個啟發：能否用一個時序狀態機模型來表達它？VT01用時態邏輯狀態機表達領域模型 VT01用時態邏輯狀態機表達領域模型 理解幾個基本概念 Safety：表征一個系統不符合要求的事件一定不能發生 Liveness：表征一個系統符合要求

6、的事件最終一定要發生 時態邏輯狀態機公式=Init/Safety/Liveness 用不變式檢查模型歸納性質 題目：求兩個自然數的最大公約數，驗證歐幾里德算法正確性 用不變式檢查模型歸納性質 能保證算法是正確的嗎？結果是正確的并不代表算法每一步都是對的，因此上面的不變式只能保證算法部分正確性。保證算法全局正確性的不變式需要滿足可歸納性，數學公式必須滿足：用不變式檢查模型歸納性質 正確的不變式是什么？結論：不變式檢查主要是針對可歸納性全局狀態屬性 用線性時態邏輯檢查模型正確性 題目：求兩個自然數的最大公約數，驗證歐幾里德算法正確性 用線性時態邏輯檢查模型正確性 正確性屬性需要考慮哪些因素？一個真

7、實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 ACRN背景簡介：ACRN是Linux基金會今年發布的一款新的嵌入式hypervisor參考軟件，項目的官方名稱為ACRN，這是一個專為物聯網和嵌入式設備設計的管理程序。該項目得益于英特爾代碼和工程的貢獻，其目標是創建一個靈活小巧的虛擬機管理系統。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 InterruptWindow機制流程圖 虛擬機接收到外部中斷產生VM_Exi

8、t事件退出到Hypervisor將外部中斷轉換為虛擬中斷并計算虛擬中斷優先級當前虛擬機是否開中斷？當前最高優先級虛擬中斷注入虛擬機返回虛擬機運行狀態啟動InterruptWindow機制是否一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 InterruptWindow機制流程圖 虛擬機執行STI指令是否開啟InterruptWindow機制？產生VM_Exit事件退出到Hypervisor重新計算虛擬機虛擬中斷優先級注入最高優先級中斷到虛擬機返回虛擬機執行狀態繼續執行是否一個真實的例子-Intel AC

9、RN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 形式化領域模型 InterruptWindowInterruptWindow領域模型六要素：領域模型六要素：虛擬機運行狀態虛擬機運行狀態 VM_ExitVM_Exit事件處理事件處理 外部中斷處理外部中斷處理 虛擬中斷計算與分發虛擬中斷計算與分發 InterruptWindowInterruptWindow計算計算 模型運行起來模型運行起來 一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 構建虛擬

10、機運行狀態模型 虛擬機運行狀態三要素：虛擬機運行狀態三要素：響應外部中斷響應外部中斷 虛擬中斷執行虛擬中斷執行 InterruptWindow檢測與處理檢測與處理 箴言：在箴言：在LTLLTL邏輯里面我們使用一個外部中斷集合邏輯里面我們使用一個外部中斷集合來表達外部中斷在虛擬機運行階段的響應動作，使來表達外部中斷在虛擬機運行階段的響應動作，使用虛擬中斷集合來表達虛擬中斷控制器。用虛擬中斷集合來表達虛擬中斷控制器。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 構建虛擬機運行狀態模型 一個真實的例子-In

11、tel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 VM_Exit事件處理 如果如果IRRIRR集合為空表明沒有虛擬中斷需要注入則集合為空表明沒有虛擬中斷需要注入則irq_window_enabledirq_window_enabled需要關閉使能，然后跳轉需要關閉使能，然后跳轉到下一個狀態到下一個狀態l3l3繼續處理繼續處理 一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 外部中斷處理 ACRNACRN針對外部中斷的處理主要是放在針對

12、外部中斷的處理主要是放在softirqsoftirq軟中斷處理軟中斷處理過程執行，這部分我們只完成一個操作那就是從過程執行，這部分我們只完成一個操作那就是從external_interruptsexternal_interrupts集合里面取出一個中斷放入集合里面取出一個中斷放入pending_intrpending_intr集合，模擬實際硬件的動作，執行完成后集合，模擬實際硬件的動作，執行完成后跳轉到下一個狀態跳轉到下一個狀態l4l4。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 虛擬中斷計算與分發

13、 acrnacrn代碼設計是放在代碼設計是放在acrn_do_intr_processacrn_do_intr_process過程中實現，過程中實現，我們的數學抽象是從我們的數學抽象是從pending_intrpending_intr集合中取出一個中斷然集合中取出一個中斷然后加入到后加入到vapicvapic集合中，完成虛擬中斷的計算與分發注入集合中，完成虛擬中斷的計算與分發注入動作，處理完成后繼續跳轉到下一個狀態動作，處理完成后繼續跳轉到下一個狀態l5l5。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗

14、證 InterruptWindow計算 邏輯邏輯模型：模型：執行完畢則跳轉到執行完畢則跳轉到l1l1即即vm_runvm_run狀態模擬狀態模擬vm_entryvm_entry指令動作進入虛擬機運行態指令動作進入虛擬機運行態，直接看公式，直接看公式模型可以很容易理解。模型可以很容易理解。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 模型怎樣跑起來？心法：心法：InterruptWindowInterruptWindow模型模型是可被多個是可被多個VCPUVCPU線程重入的并發線程重入的并發處理模型，因

15、此需要針對該代碼模型進行死鎖或異常運行檢處理模型，因此需要針對該代碼模型進行死鎖或異常運行檢查，這是確保安全性的關鍵要素之一，需要我們基于查，這是確保安全性的關鍵要素之一，需要我們基于該領域該領域模型的推導進一步構造出并發處理模型的數學描述，模型的推導進一步構造出并發處理模型的數學描述，LTLLTL是將是將并發模型表示為時序狀態的不確定性組合，因此我們可以使并發模型表示為時序狀態的不確定性組合，因此我們可以使用時態邏輯狀態機模型來表達這種不確定性組合用時態邏輯狀態機模型來表達這種不確定性組合。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN Interr

16、uptWindow軟件模型正確性驗證 實現：我們可以設計一個時序狀態機讓這些時序狀態并發實現：我們可以設計一個時序狀態機讓這些時序狀態并發運行起來。運行起來。一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型正確性驗證 InterruptWindowInterruptWindow模型安全性檢查：模型安全性檢查：終止性檢查終止性檢查 正確性檢查正確性檢查 形式化模型驗證 正確性檢查：正確性檢查：結果正確性結果正確性 過程正確性過程正確性 一個真實的例子-Intel ACRN InterruptWindowIntel A

17、CRN InterruptWindow軟件模型正確性驗證 結果正確性結果正確性 如果當前如果當前VCPUVCPU除了當前中斷還有其他中斷要處理并且除了當前中斷還有其他中斷要處理并且VCPUVCPU處于運行態，那么必須使能處于運行態，那么必須使能InterruptWindowInterruptWindow機機制。制。過程正確性過程正確性 即任意一個即任意一個VCPUVCPU的的pending_intrpending_intr和和vapicvapic集合都為空集合都為空 一個真實的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow軟件模型

18、正確性驗證 深入學習：可以參考我發表的文章 ACRN之InterruptWindow功能正確性形式化驗證 怎樣用形式化技術推導一個正確模型 理論方法 理論方法 I.I.將原始需求描述進一步抽象使用一階數理邏輯將原始需求描述進一步抽象使用一階數理邏輯+集合論建立頂層數集合論建立頂層數理邏輯模型，該模型即是需求的數學規格化描述，是進一步設計理邏輯模型，該模型即是需求的數學規格化描述，是進一步設計求精和驗證的依據。求精和驗證的依據。II.II.根據頂層數理邏輯模型做設計求精展開成線性時態邏輯表達式，根據頂層數理邏輯模型做設計求精展開成線性時態邏輯表達式，建立時態邏輯規格化描述。建立時態邏輯規格化描述

19、。III.III.如需求涉及到并發體描述則將并發體抽象成時態邏輯加入第二步如需求涉及到并發體描述則將并發體抽象成時態邏輯加入第二步線性時態邏輯規格化描述中。線性時態邏輯規格化描述中。IV.IV.根據需求描述建立時態邏輯屬性和數學不變式對線性時態邏輯規根據需求描述建立時態邏輯屬性和數學不變式對線性時態邏輯規格化描述進行模型驗證。格化描述進行模型驗證。物聯網操作系統內存管理模型設計推導物聯網操作系統內存管理模型設計推導 一個實際案例 物聯網操作系統zephyr內存管理模型設計推導 Zephyr內存分配器定義：a.a.內存池定義：內存池是一顆四叉樹，樹中每個結點代表內存池定義：內存池是一顆四叉樹，樹

20、中每個結點代表一個物理內存塊，每層結點內存塊尺寸相同，從樹根到一個物理內存塊，每層結點內存塊尺寸相同，從樹根到葉子結點每層內存塊尺寸按照從大到小降序排列。葉子結點每層內存塊尺寸按照從大到小降序排列。b.b.根據用戶指定的內存塊大小在內存池中選擇一塊合適尺根據用戶指定的內存塊大小在內存池中選擇一塊合適尺寸的內存塊輸出。寸的內存塊輸出。c.c.如果當前內存池沒有合適大小的內存塊則嘗試對當前最如果當前內存池沒有合適大小的內存塊則嘗試對當前最大尺寸內存塊進行裂解找到合適內存塊輸出，如果裂解大尺寸內存塊進行裂解找到合適內存塊輸出，如果裂解失敗則報錯。失敗則報錯。d.d.允許多個線程并發訪問該功能接口。允

21、許多個線程并發訪問該功能接口。頂層邏輯設計頂層邏輯設計 內存池模型設計：內存池模型設計：這里我們選用這里我們選用TLA+TLA+的的Record+FunctionRecord+Function模型來表達這一概念模型來表達這一概念如下：如下：k_mem_poolk_mem_pool為一個為一個recordrecord模型，模型，max_szmax_sz是這顆四叉樹頂層最是這顆四叉樹頂層最大內存塊尺寸，大內存塊尺寸，levelslevels是一個是一個functionfunction用來表示樹的每一層擁用來表示樹的每一層擁有的空閑內存塊，每一層空閑塊用集合來表達。有的空閑內存塊，每一層空閑塊用集合

22、來表達。頂層邏輯設計頂層邏輯設計 兩個核心概念：兩個核心概念：合適尺寸的內存塊合適尺寸的內存塊 裂解概念裂解概念 頂層邏輯設計頂層邏輯設計 裂解基本原理：裂解基本原理：裂解過程需要一個基于樹的層次區間進行，那么我們就必裂解過程需要一個基于樹的層次區間進行，那么我們就必須要首先求出需要裂解層次的須要首先求出需要裂解層次的start_levelstart_level和和end_levelend_level，可以，可以分別定義為分別定義為free_levelfree_level、alloc_levelalloc_level，然后我們根據這個區間，然后我們根據這個區間設計一套數學公式來表達這個裂解過程

23、。設計一套數學公式來表達這個裂解過程。頂層邏輯設計頂層邏輯設計 線性時態邏輯模型求精 求精策略：根據頂層邏輯模型的規格化描述，我們將公式里求精策略：根據頂層邏輯模型的規格化描述，我們將公式里面的面的OPERATOROPERATOR進一步展開成狀態流用時態邏輯進行表達。進一步展開成狀態流用時態邏輯進行表達。技巧性原則：如需求描述涉及到并發體訪問則先不考慮并發技巧性原則：如需求描述涉及到并發體訪問則先不考慮并發因素，例如我們本例模型可以先考慮非并發模型的求精過程，因素，例如我們本例模型可以先考慮非并發模型的求精過程，之后再逐步加入針對并發體訪問邏輯的時序狀態描述，實踐之后再逐步加入針對并發體訪問邏

24、輯的時序狀態描述，實踐證明這樣求精的效率非常高。證明這樣求精的效率非常高。線性時態邏輯模型求精 非并發的時態邏輯求精如下：非并發的時態邏輯求精如下：線性時態邏輯模型求精 終止性驗證 技術原則：驗證過程中如果存在問題在此基礎上進行技術原則：驗證過程中如果存在問題在此基礎上進行調試修改，驗證通過后我們再增加針對并發體的時態調試修改，驗證通過后我們再增加針對并發體的時態邏輯。邏輯。并發體時態邏輯并發體時態邏輯 并發體時態邏輯并發體時態邏輯 并發體終止性驗證并發體終止性驗證 正確性驗證正確性驗證 化簡化簡:N個線程同時從初始化四叉樹模型中申請大小相同的內存塊所要滿足的預期屬性 進一步規格化描述進一步規

25、格化描述 初始化四叉樹模型：初始化四叉樹模型：N N個線程申請內存塊大?。簜€線程申請內存塊大?。侯A期屬性：預期屬性：正確性驗證正確性驗證 出錯了？正確性驗證正確性驗證 原因分析 原因一：四叉樹裂解過程中當前層內存塊的提取到原因一：四叉樹裂解過程中當前層內存塊的提取到下一層內存塊的裂解之間的操作存在時間空隙可以下一層內存塊的裂解之間的操作存在時間空隙可以被其他線程所搶占，這樣會導致內存分配不正確導被其他線程所搶占，這樣會導致內存分配不正確導致時序狀態違例。致時序狀態違例。原因二：原因二：L3L3狀態分配內存可以被其他線程所搶占造狀態分配內存可以被其他線程所搶占造成當前線程內存分配計算的成當前線程

26、內存分配計算的free_lfree_l、alloc_lalloc_l游標與被游標與被搶占后的四叉樹模型不一致從而導致內存分配失敗搶占后的四叉樹模型不一致從而導致內存分配失敗產生時序違例。產生時序違例。正確性驗證正確性驗證 解決方案 針對這兩種情況我們考慮將針對這兩種情況我們考慮將L3L3、L4L4狀態進一步優化狀態進一步優化如下：如下：正確性驗證正確性驗證 再次驗證！通過！總結總結 我們的方法雖然只能做到部分形式化，但是基本上工作量已經非常小了，而且項目和設計人員非常容易掌控，最后經過簡單的目標測試就可以完成產品目標代碼最終的驗證工作。需求形式化、設計形式化、驗證形式化：軟件設計初期往往充滿了很多不確定因素，包括對需求概念的理解、原始需求模型的安全性、正確性考慮都不可能做到完全充分清晰的前提下，使用形式化方法從頂層邏輯模型設計階段就將需求概念模型進行精確描述，那么錯誤的模型或在求精階段存在的BUG就可以通過時態邏輯的屬性驗證發現并進行修改優化。上下一致、驗證模型容易向目標代碼轉換：線性時態邏輯是作為頂層邏輯模型的求精，既保證了與頂層需求模型的一致性同時又保證了求精模型可以在實現層面很容易向目標代碼轉換。部分形式化大大減少工作量：深入實踐深入實踐 基于線性時態邏輯的物聯網操作系統安全性設計理論。推薦兩本書：THANK YOU