• 
    

    
    

      99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

      基于有限狀態(tài)機(jī)的操作系統(tǒng)需求層形式化驗(yàn)證*

      2019-05-17 09:47:38張錦坤楊孟飛
      關(guān)鍵詞:狀態(tài)機(jī)中斷全局

      張錦坤,楊孟飛,喬 磊,3,楊 樺,劉 波

      0 引 言

      隨著航天事業(yè)的迅猛發(fā)展,空間任務(wù)的規(guī)模及復(fù)雜度上升,空間飛行器上的軟件規(guī)模也隨之增加.操作系統(tǒng)作為計(jì)算機(jī)系統(tǒng)中硬件和軟件資源的管理者,其可靠性和和安全性也越發(fā)重要.操作系統(tǒng)中的任何一個(gè)微小的錯(cuò)誤都可能導(dǎo)致整個(gè)系統(tǒng)的崩潰,因此操作系統(tǒng)應(yīng)該是一個(gè)高可靠、高可信的軟件系統(tǒng),這是保證所有應(yīng)用軟件能可靠運(yùn)行的基礎(chǔ).形式化方法[1]逐漸成為航天器操作系統(tǒng)可信性的有效保障,采用形式化的方法對操作系統(tǒng)進(jìn)行設(shè)計(jì)和驗(yàn)證[2-5]已經(jīng)得到國際學(xué)術(shù)界的廣泛重視.

      國內(nèi)外對操作系統(tǒng)的形式化驗(yàn)證開展了一些研究,澳大利亞的NICTA實(shí)驗(yàn)室對操作系統(tǒng)內(nèi)核L4開展了形式化驗(yàn)證工作,并發(fā)布了新一代嵌入式操作系統(tǒng)seL4[6-7];耶魯大學(xué)的邵中將自動化定理證明的優(yōu)點(diǎn)與基于VeriML/OCAP的認(rèn)證編程框架的模塊化表達(dá)相結(jié)合[8],對可驗(yàn)證的安全內(nèi)核做了一定的研究;馮新宇等人開發(fā)了一個(gè)驗(yàn)證操作系統(tǒng)的框架[9-10],提出了對內(nèi)核建模和全局性質(zhì)驗(yàn)證的方法;NELSON等人介紹了一種關(guān)于OS內(nèi)核的設(shè)計(jì)、實(shí)現(xiàn)和形式化驗(yàn)證的方法[11],用Z3 SMT solver檢驗(yàn)了50個(gè)系統(tǒng)調(diào)用和陷阱處理;WEN SU和JEAN-RAYMOND ABRIAL等人用Event-B方法形式化開發(fā)了一個(gè)實(shí)時(shí)系統(tǒng)的內(nèi)存管理模塊[12-13];錢振江等人對安全操作系統(tǒng)的形式化驗(yàn)證做了相關(guān)研究[14-18],采用操作系統(tǒng)對象語義模型(OSOSM)對系統(tǒng)的設(shè)計(jì)進(jìn)行形式化建模;北京控制工程研究所也對操作系統(tǒng)的形式化驗(yàn)證做了一定的研究[19-22],用Event-B方法對操作系統(tǒng)的一些模塊進(jìn)行了形式化建模和驗(yàn)證.不過當(dāng)前對操作系統(tǒng)形式化驗(yàn)證的研究工作要么是針對單個(gè)模塊,要么是從代碼反推需求規(guī)約,自上而下的從需求到設(shè)計(jì)再到實(shí)現(xiàn)層的完整的形式化驗(yàn)證還比較少.需求層的形式化驗(yàn)證是操作系統(tǒng)形式化驗(yàn)證的一部分,能夠更早地發(fā)現(xiàn)是否有潛在的錯(cuò)誤,有助于完成整個(gè)操作系統(tǒng)的形式化驗(yàn)證,確保整個(gè)操作系統(tǒng)的安全性和可靠性.

      航天器計(jì)算機(jī)系統(tǒng)一般采用中斷驅(qū)動型多任務(wù)并發(fā)嵌入式操作系統(tǒng),其系統(tǒng)結(jié)構(gòu)復(fù)雜,具有多任務(wù)并發(fā)、中斷頻發(fā)且嵌套、時(shí)序固定等特性.圖1示例了一個(gè)典型系統(tǒng),包括6個(gè)任務(wù)(4個(gè)固定任務(wù),2個(gè)隨機(jī)任務(wù)),4個(gè)中斷(2個(gè)周期性中斷,2個(gè)隨機(jī)中斷).4個(gè)任務(wù)都必須在固定時(shí)間點(diǎn)啟動,所有任務(wù)必須在規(guī)定時(shí)間期限內(nèi)完成.針對這類軟件的主要驗(yàn)證技術(shù)包括測試技術(shù)和形式化技術(shù).測試是目前保證可靠性而廣泛使用的技術(shù),但系統(tǒng)運(yùn)行的狀態(tài)空間大,測試能發(fā)現(xiàn)問題,但不能說明沒有問題,無法從根本上保障操作系統(tǒng)的可靠性.而形式化驗(yàn)證是使用邏輯推理系統(tǒng)來保證計(jì)算機(jī)程序正確性的方法之一.通過形式化的程序邏輯來驗(yàn)證程序是否滿足給定規(guī)范,并通過顯式的證明來使用戶確信驗(yàn)證結(jié)果的正確性,是保證軟件可信性的有效方法之一,將成為更加有效實(shí)現(xiàn)“零缺陷”的技術(shù).

      圖1 中斷驅(qū)動型多任務(wù)并發(fā)操作系統(tǒng)Fig.1 Interrupt-driven multitasking concurrent operating system

      本文在分析某典型航天器操作系統(tǒng)SpaceOS2需求的基礎(chǔ)上,利用有限狀態(tài)機(jī)方法進(jìn)行形式化建模,給出全局性質(zhì)的形式化定義,并在Coq中進(jìn)行了形式化驗(yàn)證.證明顯示SpaceOS2在需求層滿足提出的全局性質(zhì).

      1 系統(tǒng)需求

      操作系統(tǒng)的需求是硬件加電后能夠執(zhí)行調(diào)度器軟件,在規(guī)定的資源和時(shí)間要求下調(diào)度器對任務(wù)進(jìn)行調(diào)度執(zhí)行,并且能夠響應(yīng)中斷.在整個(gè)運(yùn)行過程中,操作系統(tǒng)還應(yīng)該滿足一些全局性質(zhì),確保任務(wù)的安全順利執(zhí)行.

      1.1 系統(tǒng)組成

      操作系統(tǒng)根據(jù)系統(tǒng)功能可以劃分為7個(gè)部分,初始化、任務(wù)管理、中斷管理、時(shí)間管理、內(nèi)存管理、任務(wù)間通信管理和外設(shè)管理,如表1所示.

      表1 不同組成部分及其功能Tab.1 Different components and their functions

      其中任務(wù)管理、中斷管理和時(shí)間管理這3個(gè)模塊構(gòu)成了最小系統(tǒng),可以反映操作系統(tǒng)最基本的行為特征,針對安全關(guān)鍵系統(tǒng)的操作系統(tǒng)模式可以完全覆蓋,這樣既簡化了系統(tǒng)模型,又涵蓋了所有核心要素,便于建模與驗(yàn)證.

      1.2 任務(wù)狀態(tài)

      任務(wù)狀態(tài)反映任務(wù)執(zhí)行過程的變化,這些狀態(tài)隨著任務(wù)的執(zhí)行和外部條件的變化而轉(zhuǎn)換.操作系統(tǒng)中,任務(wù)狀態(tài)一般包含以下5種:就緒態(tài)、阻塞態(tài)、掛起態(tài)、睡眠態(tài)和運(yùn)行態(tài).本文針對典型的航天器操作系統(tǒng)工程應(yīng)用,其任務(wù)狀態(tài)包括就緒態(tài)、運(yùn)行態(tài)和掛起態(tài)三個(gè)核心狀態(tài).

      (1)就緒態(tài)(Ready):處于此狀態(tài)的任務(wù)除了等待CPU外,不需要等待其他資源;

      (2)阻塞態(tài)(Pend):由于一些資源不可用而阻塞的狀態(tài)(等待信號量、消息);

      (3)掛起態(tài)(Suspend):任務(wù)進(jìn)行了掛起操作的狀態(tài).

      圖2 任務(wù)狀態(tài)轉(zhuǎn)移Fig.2 Task state transition

      1.3 系統(tǒng)狀態(tài)

      隨著任務(wù)的執(zhí)行和外部條件的變化,操作系統(tǒng)狀態(tài)也在發(fā)生著變化.系統(tǒng)狀態(tài)包括兩部分,一是任務(wù)列表,也就是各個(gè)任務(wù)的狀態(tài);二是其他外部條件的狀態(tài),比如中斷開或關(guān).根據(jù)不同時(shí)刻任務(wù)狀態(tài)的不同,系統(tǒng)狀態(tài)也不盡相同.

      1.4 全局性質(zhì)

      操作系統(tǒng)應(yīng)該滿足一些全局性質(zhì),不僅在初始狀態(tài)滿足,并且系統(tǒng)由初始狀態(tài)執(zhí)行動作到達(dá)的任意狀態(tài)依然保持滿足.本文分別從任務(wù)、中斷和時(shí)間3方面考慮,提煉出6條核心全局性質(zhì),即在驗(yàn)證過程中需要證明的定理:

      (1)系統(tǒng)中有且只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài);

      (2)運(yùn)行任務(wù)掛起放棄CPU后只能進(jìn)入掛起態(tài);

      (3)控制周期中斷和時(shí)間片中斷不能同時(shí)發(fā)生;

      (4)任務(wù)狀態(tài)不能直接從就緒態(tài)轉(zhuǎn)為掛起態(tài);

      (5)只能在任務(wù)啟動點(diǎn)調(diào)度新任務(wù);

      (6)空閑任務(wù)不能在啟動點(diǎn)調(diào)度.

      其中任務(wù)啟動點(diǎn)指的是每個(gè)應(yīng)用任務(wù)劃分好的固定時(shí)間片的啟動時(shí)刻,在每個(gè)任務(wù)啟動點(diǎn)調(diào)度執(zhí)行對應(yīng)的應(yīng)用任務(wù).

      2 有限狀態(tài)機(jī)建模方法

      有限狀態(tài)機(jī)[23]是描述有限個(gè)系統(tǒng)狀態(tài)以及在這些狀態(tài)之間的轉(zhuǎn)移和動作等行為的數(shù)學(xué)模型,現(xiàn)已被廣泛應(yīng)用于計(jì)算機(jī)科學(xué)、軟件工程和自動控制等領(lǐng)域,成為計(jì)算機(jī)軟件、硬件和網(wǎng)絡(luò)及控制等系統(tǒng)常見的形式化模型之一.有限狀態(tài)機(jī)可以很好地表達(dá)并發(fā)行為,適合并發(fā)系統(tǒng)的刻畫,能夠精確表現(xiàn)系統(tǒng)狀態(tài)之間的遷移;而且狀態(tài)機(jī)方法易于書寫、驗(yàn)證,也容易轉(zhuǎn)變成設(shè)計(jì)或程序代碼.不過在面臨較大規(guī)模系統(tǒng)的時(shí)候,有限狀態(tài)機(jī)建模將會十分繁瑣和復(fù)雜.

      在操作系統(tǒng)需求層,可以忽略掉底層的細(xì)節(jié),舍去復(fù)雜數(shù)據(jù)結(jié)構(gòu)進(jìn)行化簡,從而在頂層抽象出一個(gè)有限狀態(tài)機(jī)模型來研究系統(tǒng)運(yùn)行過程.一個(gè)有限狀態(tài)機(jī)可以由一個(gè)五元組[24]表示:

      M=(Q,∑,q0,F(xiàn),δ)

      其中,Q是系統(tǒng)狀態(tài)的非空有限集合;∑是輸入信息或條件的集合;q0是初始狀態(tài)且q0∈S;δ是狀態(tài)轉(zhuǎn)移函數(shù),可以表示為δ:Q×∑→Q.在一般的有限狀態(tài)機(jī)模型中,存在一個(gè)終止?fàn)顟B(tài)軟件集合F,且F?S,經(jīng)過一段時(shí)間的運(yùn)行后,狀態(tài)機(jī)歷經(jīng)一些狀態(tài)遷移,到達(dá)運(yùn)行的最后狀態(tài)F.但是操作系統(tǒng)是一個(gè)連續(xù)運(yùn)行的軟件,在啟動之后就永遠(yuǎn)執(zhí)行,有外部終止操作的話恢復(fù)到初始狀態(tài),不存在終止?fàn)顟B(tài).因此本文采用的狀態(tài)機(jī)由四元組表示:

      M=(Q,∑,q0,δ)

      2.1 系統(tǒng)狀態(tài)集合

      操作系統(tǒng)在運(yùn)行過程中只能處于某一個(gè)已知的確定狀態(tài),比如在狀態(tài)q0,任務(wù)0(即空閑任務(wù))處于運(yùn)行態(tài)而其他任務(wù)都處于掛起態(tài);在qm狀態(tài)時(shí),任務(wù)m處于運(yùn)行態(tài)而其他任務(wù)都處于掛起態(tài).同時(shí)在不同狀態(tài)下,其他外部環(huán)境也有所差異,比如是否允許時(shí)間片中斷等.不同時(shí)刻的系統(tǒng)狀態(tài)組成了系統(tǒng)狀態(tài)集合.

      2.2 輸入條件

      操作系統(tǒng)在運(yùn)行過程中接受某一確定的輸入值,根據(jù)這些輸入值采取不同的動作.這些輸入值包括控制周期中斷、時(shí)間片中斷和任務(wù)提前結(jié)束等.

      2.3 初始狀態(tài)

      操作系統(tǒng)經(jīng)過初始化后,創(chuàng)建了若干任務(wù),可以執(zhí)行調(diào)度器軟件并響應(yīng)緊急事件.此時(shí)系統(tǒng)處于初始狀態(tài)q0:空閑任務(wù)處于運(yùn)行態(tài),其他任務(wù)都處于掛起態(tài);并且系統(tǒng)在等待第一個(gè)輸入值.

      2.4 狀態(tài)轉(zhuǎn)移函數(shù)

      狀態(tài)轉(zhuǎn)移函數(shù)表示操作系統(tǒng)的狀態(tài)轉(zhuǎn)移規(guī)則.某一時(shí)刻操作系統(tǒng)處于某一狀態(tài)qn,同時(shí)接收到某一輸入值an,則通過函數(shù)δ可以推出下一時(shí)刻操作系統(tǒng)的狀態(tài)為qm=(qn,an).按照圖1所示的操作系統(tǒng),每個(gè)任務(wù)劃分好時(shí)間片,在固定時(shí)間點(diǎn)按周期運(yùn)行,因此在任一時(shí)刻下,每個(gè)任務(wù)的狀態(tài)都是確定的,并且中斷狀態(tài)也是確定的,那么按照本文定義,系統(tǒng)狀態(tài)也是確定的,不存在一個(gè)事件對應(yīng)多個(gè)動作的情況,即狀態(tài)機(jī)是確定有限狀態(tài)機(jī).

      3 SpaceOS2建模

      SpaceOS2是由北京控制工程研究所研制的第二代航天嵌入式實(shí)時(shí)操作系統(tǒng),在多個(gè)航天型號任務(wù)上得到了實(shí)際應(yīng)用.本文將有限狀態(tài)機(jī)建模方法應(yīng)用于在航天器上廣泛應(yīng)用的SpaceOS2,為系統(tǒng)狀態(tài)機(jī)模型進(jìn)行形式化建模包含兩部分工作:一是描述內(nèi)核狀態(tài)和輸入條件,即狀態(tài)集合和轉(zhuǎn)移條件;二是描述內(nèi)核操作的抽象規(guī)范,即狀態(tài)轉(zhuǎn)移函數(shù).

      3.1 內(nèi)核狀態(tài)和輸入條件

      (TaskState)state::=R(ready)|E(running)|S(suspend)

      (Tasklist)tasklist::=nil|state list

      (Controlflag)controlflag ::=True|False

      (Timesliceflag)timesliceflag::=True|False

      (Systate)systate::={tasklist,controlflag,timesliceflag}

      (Time)t∈Nat

      (TimeStart) ts∈Nat

      (Event)event::=IntControl (t)| IntTimeslice(t)| TaskEnd(t)

      SpaceOS2系統(tǒng)狀態(tài)systate包含3部分:任務(wù)列表tasklist,控制周期中斷響應(yīng)標(biāo)志controlflag和時(shí)間片中斷響應(yīng)標(biāo)志timesliceflag.任務(wù)列表tasklist是所有任務(wù)的任務(wù)狀態(tài)列表,每個(gè)系統(tǒng)狀態(tài)對應(yīng)一個(gè)任務(wù)列表.任務(wù)狀態(tài)有三種類型:就緒態(tài)、運(yùn)行態(tài)和掛起態(tài).操作系統(tǒng)響應(yīng)的中斷有兩種,控制周期中斷和時(shí)間片中斷,根據(jù)是否響應(yīng)某種中斷,標(biāo)志為Ture或者False兩種狀態(tài).事件包含3類:控制周期中斷IntControl、時(shí)間片中斷IntTimeslice和任務(wù)提前結(jié)束TaskEnd,并且?guī)в袝r(shí)間t,時(shí)間t是離散自然數(shù).ts指的是任務(wù)啟動點(diǎn)應(yīng)用于某航天器的SpaceOS2在初始化時(shí)創(chuàng)建了12個(gè)任務(wù),依次為10個(gè)應(yīng)用任務(wù),1個(gè)空閑任務(wù)和1個(gè)系統(tǒng)任務(wù).其中系統(tǒng)任務(wù)總是處于掛起態(tài),其他11個(gè)任務(wù)在不同時(shí)刻處于運(yùn)行態(tài)時(shí),對應(yīng)不同的系統(tǒng)狀態(tài).

      初始狀態(tài)下只有空閑任務(wù)處于運(yùn)行態(tài),其他任務(wù)處于掛起態(tài),因此初始任務(wù)列表定義為:init_tasklist::=(S,S,S,S,S,S,S,S,S,S,E,S).并且初始狀態(tài)在等待控制周期中斷到來,不允許時(shí)間片中斷,所以初始狀態(tài)s0定義為:

      init_state(s0)::={tasklist=init_tasklist,controlflag=True,timesliceflag=False}

      控制周期中斷到來之后,時(shí)間片中斷開關(guān)打開,其他任務(wù)開始調(diào)度執(zhí)行,任務(wù)n(1≤n≤10)處于運(yùn)行態(tài)時(shí)對應(yīng)的任務(wù)列表tasklist_n中,第n個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài)E,空閑任務(wù)處于就緒態(tài)R,其他任務(wù)處于掛起態(tài).系統(tǒng)狀態(tài)可以定義為:

      state_n(sn)::={tasklist=tasklist_n,controlflag=False,timesliceflag = True }

      此外當(dāng)應(yīng)用任務(wù)在時(shí)間片中斷到來之前提前結(jié)束時(shí),空閑任務(wù)執(zhí)行,其他任務(wù)掛起,此時(shí)的任務(wù)列表和初始任務(wù)列表相同,但是當(dāng)前狀態(tài)允許響應(yīng)時(shí)間片中斷而不響應(yīng)控制周期中斷,因此這是一個(gè)不同于初始狀態(tài)的中間狀態(tài)state_M:

      state_M(sm)::={tasklist=init_tasklist,controlflag=False,timesliceflag = True }

      至此得到所有的12個(gè)系統(tǒng)狀態(tài),Q={s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,sM}.

      3.2 狀態(tài)轉(zhuǎn)移函數(shù)

      確定了各個(gè)狀態(tài)以及相關(guān)條件后,還要確立各個(gè)狀態(tài)之間的轉(zhuǎn)換關(guān)系.操作系統(tǒng)啟動之后進(jìn)行初始化,處于初始狀態(tài),控制周期中斷到來之后,轉(zhuǎn)移到s1狀態(tài)并開始時(shí)間片計(jì)數(shù),允許響應(yīng)時(shí)間片中斷.之后每4 ms來一個(gè)時(shí)間片中斷,如果此時(shí)刻是新任務(wù)的啟動點(diǎn)(ts)則轉(zhuǎn)換到下一個(gè)狀態(tài);否則繼續(xù)執(zhí)行當(dāng)前任務(wù).另外如果任務(wù)提前結(jié)束,則切換到空閑任務(wù)執(zhí)行,進(jìn)入sM狀態(tài).40個(gè)時(shí)間片之后,不再響應(yīng)時(shí)間片中斷,回到初始狀態(tài)等待下一個(gè)控制周期中斷到來.具體的狀態(tài)轉(zhuǎn)移圖如圖3所示,其中IntControl代表控制周期中斷,TE代表事件任務(wù)提前結(jié)束(TaskEnd),IT和ITS都是時(shí)間片中斷(IntTimeslice),ITS代表當(dāng)前中斷時(shí)刻是新任務(wù)的啟動點(diǎn).

      圖3 狀態(tài)轉(zhuǎn)移圖Fig.3 State transition diagram

      結(jié)合狀態(tài)轉(zhuǎn)移圖并進(jìn)行規(guī)約后,給出狀態(tài)轉(zhuǎn)移函數(shù)的定義,涉及到兩個(gè)參數(shù),一個(gè)是帶時(shí)間的事件類型,另外一個(gè)是當(dāng)前的系統(tǒng)狀態(tài).

      圖4 狀態(tài)轉(zhuǎn)移函數(shù)Fig.4 State transition function

      4 形式化驗(yàn)證

      在采用了有限狀態(tài)機(jī)方法對SpaceOS2進(jìn)行了形式化描述和建模之后,接下來要采用合適的工具對其進(jìn)行形式化驗(yàn)證.Coq是目前國際上交互式定理證明領(lǐng)域的主流工具,本文選擇定理證明工具Coq來進(jìn)行驗(yàn)證,首先要對應(yīng)地在Coq中對模型進(jìn)行描述,然后對提煉出的性質(zhì)進(jìn)行形式化定義并且采用恰當(dāng)?shù)淖C明策略進(jìn)行驗(yàn)證,說明操作系統(tǒng)SpaceOS2在需求層滿足提出的全局性質(zhì).

      4.1 內(nèi)核建模

      為了驗(yàn)證操作系統(tǒng)是否滿足提出的全局性質(zhì),要根據(jù)第3節(jié)建立的有限狀態(tài)機(jī)模型在Coq中相應(yīng)地進(jìn)行描述建模.因?yàn)榻⒌膸r(shí)間的事件驅(qū)動任務(wù)轉(zhuǎn)移系統(tǒng)模型,要依次定義時(shí)間、轉(zhuǎn)移事件、任務(wù)狀態(tài)和系統(tǒng)狀態(tài)等類型,并且構(gòu)造狀態(tài)轉(zhuǎn)移函數(shù)transfer.涉及到的參數(shù)有帶時(shí)間的事件類型和前一個(gè)狀態(tài).在3種事件驅(qū)動下,進(jìn)行固定時(shí)間點(diǎn)的任務(wù)調(diào)度轉(zhuǎn)移.

      4.2 性質(zhì)描述

      要驗(yàn)證系統(tǒng)模型是否滿足全局性質(zhì),首先要明確證明目標(biāo),即在Coq環(huán)境下要給出性質(zhì)的定義.形式化描述全局性質(zhì)時(shí),首先將性質(zhì)涉及到的數(shù)據(jù)結(jié)構(gòu)從內(nèi)核狀態(tài)中取出,然后描述這些數(shù)據(jù)結(jié)構(gòu)之間的關(guān)系.在此給出幾條性質(zhì)的形式化描述,在Coq中驗(yàn)證時(shí)根據(jù)此描述進(jìn)行相應(yīng)的擴(kuò)充和類型定義.

      性質(zhì)1 有且只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài)

      ? systate,count (state = running)=1

      性質(zhì)2 任務(wù)放棄CPU后只能進(jìn)入掛起態(tài)

      ? task,state =E∧event =TaskEnd?astate=S

      性質(zhì)3 控制周期中斷和時(shí)間片中斷不能同時(shí)發(fā)生

      ? systate,and (controlflag,timesliceflag)=False

      4.3 證明思路

      證明系統(tǒng)滿足一個(gè)全局性質(zhì),就要全方面考慮,不僅要證明系統(tǒng)在初始狀態(tài)滿足性質(zhì),還要證明從初始狀態(tài)執(zhí)行任意動作到達(dá)的新狀態(tài)也滿足性質(zhì).在本文建立的狀態(tài)機(jī)模型中,就是要證明操作系統(tǒng)在初始化之后的初始狀態(tài)滿足性質(zhì),并且在每個(gè)狀態(tài)之間轉(zhuǎn)換時(shí)也要滿足性質(zhì).以性質(zhì)1為例,證明思路如下:

      (1)初始狀態(tài) init_state只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài);

      (2)初始狀態(tài)轉(zhuǎn)換到s1狀態(tài),只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài);

      (3)s1狀態(tài)轉(zhuǎn)換到中間狀態(tài),只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài);

      (4)s1狀態(tài)轉(zhuǎn)換到s2狀態(tài),只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài);

      (5)中間狀態(tài)轉(zhuǎn)換到s2狀態(tài),只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài);

      (6)s1狀態(tài)轉(zhuǎn)換到s1狀態(tài),只有一個(gè)任務(wù)狀態(tài)為運(yùn)行態(tài).

      同理,按照狀態(tài)轉(zhuǎn)移圖的每一個(gè)出邊和入邊,證明每一次轉(zhuǎn)換都滿足性質(zhì)1,這樣就能保證建立的操作系統(tǒng)模型滿足該性質(zhì).

      4.4 證明策略

      明確了證明目標(biāo)和思路之后,要采取恰當(dāng)?shù)淖C明策略,將復(fù)雜的目標(biāo)進(jìn)行逐步簡化和推理,直到證明完成.以驗(yàn)證初始狀態(tài)滿足性質(zhì)1為例,首先定義了valid_state,即這個(gè)狀態(tài)下只有一個(gè)任務(wù)處于運(yùn)行態(tài).相關(guān)證明策略及推演過程如下所示.橫線之上代表此時(shí)的條件,橫線下方代表此時(shí)待證明的目標(biāo).其他5條性質(zhì)的證明與性質(zhì)1的證明類似.

      (1)intros

      通過這條證明策略,將所有條件引入證明環(huán)境,明確證明目標(biāo).此時(shí)出現(xiàn)了一個(gè)新的條件H,說明init_state的具體構(gòu)造.現(xiàn)在的證明目標(biāo)依舊是說明初始狀態(tài)為valid_state.

      1subgoal

      init_state:Rdata

      H:init_state={|TL:=init_tasklist;CF:=True;TF:=False|}

      valid_stateinit_state

      (2)rewrite H

      重寫條件H,用等號右邊項(xiàng)代替左邊項(xiàng),替換證明目標(biāo)里的init_state,進(jìn)一步將證明目標(biāo)明確.

      1subgoal

      init_state:Rdata

      H:init_state={|TL:=init_tasklist;CF:=True;TF:=False|}

      valid_state{|TL:=init_tasklist;CF:=True;TF:=False|}

      (3)unfold valid_state

      要證明初始狀態(tài)為有效狀態(tài),首先將有效狀態(tài)的定義展開,即按照之前在形式化描述時(shí)統(tǒng)計(jì)任務(wù)狀態(tài)為運(yùn)行態(tài)的任務(wù)個(gè)數(shù),證明運(yùn)行態(tài)的任務(wù)只有一個(gè).

      1subgoal

      init_state:Rdata

      H:init_state={|TL:=init_tasklist;CF:=True;TF:=False|}

      count_occtaskstate_dec(TL{|TL:=init_tasklist;CF:=True;TF:=False|})Running=1

      (4)simpl

      進(jìn)行化簡,將庫函數(shù)count_occ展開,逐個(gè)比對當(dāng)前任務(wù)列表里每一個(gè)任務(wù)狀態(tài),累計(jì)任務(wù)狀態(tài)為運(yùn)行態(tài)的任務(wù)個(gè)數(shù).

      (5)destruct (taskstate_dec Suspend Running)

      分情況討論,比較Suspend和Running兩個(gè)狀態(tài),此時(shí)引入了一個(gè)新的條件e,同時(shí)證明目標(biāo)被分解為兩個(gè)子目標(biāo),要依次驗(yàn)證這兩個(gè)子目標(biāo).

      2subgoal

      init_state:Rdata

      H:init_state={|TL:=init_tasklist;CF:=True;TF:=False|}

      e:Suspend=Running

      S(S(S(S(S(S(S(S(S(S(iftaskstate_decRunningRunningthen2else1))))))))))=1

      (iftaskstate_decRunningRunningthen1else0)=1

      (6)inversion e

      證明第一個(gè)子目標(biāo)時(shí),因?yàn)镾uspend明顯不等于Running,因此翻轉(zhuǎn)條件e,消除掉子目標(biāo)1.此時(shí)出現(xiàn)一個(gè)新的條件n.

      1subgoal

      init_state:Rdata

      H:init_state={ |TL:=init_tasklist;CF:=True;TF:=False|}

      n:Suspend<>Running

      (iftaskstate_decRunningRunningthen1else0)=1

      (7)destruct (taskstate_dec Running Running)

      分情況討論,比較Running和Running,此時(shí)又引入了一個(gè)新的條件e,同時(shí)證明目標(biāo)被分解為兩個(gè)子目標(biāo),要依次驗(yàn)證這兩個(gè)子目標(biāo).

      2subgoal

      init_state:Rdata

      H:init_state={|TL:=init_tasklist;CF:=True;TF:=False|}

      n:Suspend<>Running

      e:Running=Running

      1=1

      0=1

      (8)reflexivity

      子目標(biāo)1要證明1=1,顯式相等得證,消除掉子目標(biāo)1.此時(shí)的條件e變?yōu)闂l件n0.

      1subgoal

      init_state:Rdata

      H:init_state={|TL:=init_tasklist;CF:=True;TF:=False|}

      n:Suspend<>Running

      n0:Running<>Running

      0=1

      (9)contradiction

      子目標(biāo)的前置條件中,Running<>Running,和實(shí)際相悖,因此才得到了0=1的錯(cuò)誤結(jié)論.反證得之,消除子目標(biāo)2,至此證明完畢,初始狀態(tài)滿足性質(zhì)1.

      Nomoresubgoal

      5 結(jié) 論

      本文針對某航天器操作系統(tǒng)SpaceOS2需求層的形式化驗(yàn)證,首先確定操作系統(tǒng)需求,并由此提煉出六條核心的全局性質(zhì);然后利用有限狀態(tài)機(jī)方法進(jìn)行形式化描述,建立了一個(gè)事件驅(qū)動任務(wù)轉(zhuǎn)移系統(tǒng)模型;最后在定理證明器Coq中形式化定義全局性質(zhì),并驗(yàn)證建立的形式化模型是否滿足提出的全局性質(zhì).結(jié)果證明SpaceOS2在需求層滿足提出的全局性質(zhì),也說明采用有限狀態(tài)機(jī)方法對操作系統(tǒng)需求層進(jìn)行形式化驗(yàn)證是可行的,為進(jìn)一步全面形式化驗(yàn)證奠定了基礎(chǔ).

      猜你喜歡
      狀態(tài)機(jī)中斷全局
      Cahn-Hilliard-Brinkman系統(tǒng)的全局吸引子
      量子Navier-Stokes方程弱解的全局存在性
      基于有限狀態(tài)機(jī)的交會對接飛行任務(wù)規(guī)劃方法
      落子山東,意在全局
      金橋(2018年4期)2018-09-26 02:24:54
      跟蹤導(dǎo)練(二)(5)
      千里移防,衛(wèi)勤保障不中斷
      解放軍健康(2017年5期)2017-08-01 06:27:44
      新思路:牽一發(fā)動全局
      AT89C51與中斷有關(guān)的寄存器功能表解
      FPGA內(nèi)嵌PowerPC的中斷響應(yīng)分析
      FPGA設(shè)計(jì)中狀態(tài)機(jī)安全性研究
      英吉沙县| 平陆县| 宜兰市| 仁寿县| 鹤峰县| 涿州市| 西峡县| 林芝县| 武川县| 兖州市| 三门峡市| 玛沁县| 澎湖县| 塘沽区| 邵武市| 长沙市| 柳江县| 陆丰市| 乐昌市| 北碚区| 威远县| 息烽县| 镇康县| 改则县| 纳雍县| 会理县| 广州市| 鱼台县| 龙胜| 宁南县| 陈巴尔虎旗| 蕲春县| 肥东县| 廉江市| 平谷区| 天柱县| 荣昌县| 奎屯市| 鹤峰县| 霍城县| 黑龙江省|