• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    基于活性順序圖的形式化驗證方法及工具研究

    2016-11-23 10:02:51葉俊民趙麗嫻
    計算機測量與控制 2016年5期
    關(guān)鍵詞:自動機規(guī)約時序

    張 坤,葉俊民,王 嬙,趙麗嫻,陳 曙

    (華中師范大學  計算機學院,武漢 430079)

    基于活性順序圖的形式化驗證方法及工具研究

    張坤,葉俊民,王嬙,趙麗嫻,陳曙

    (華中師范大學計算機學院,武漢430079)

    近年來,形式化驗證方法在軟件開發(fā)過程的作用越來越大;如何充分利用形式化驗證方法提高軟件系統(tǒng)的可靠性已成為軟件開發(fā)者及使用者主要關(guān)注的問題;總結(jié)了近年來基于活性順序圖的形式化驗證方法的研究進展,首先介紹活性順序圖的語言及其表達能力與復雜性,然后深入分析現(xiàn)有的基于活性順序圖的形式化驗證的關(guān)鍵技術(shù)及其典型應(yīng)用,最后實現(xiàn)一種基于活性順序圖的運行時驗證工具,實驗證明使用本驗證工具進行形式化驗證的可行性。

    活性順序圖;形式化驗證;軟件開發(fā)過程

    0 引言

    隨著計算機技術(shù)的發(fā)展,軟件系統(tǒng)已經(jīng)滲透到人們的生活之中,軟件系統(tǒng)關(guān)系著人民的信息安全、財產(chǎn)安全乃至生命安全。形式化驗證方法在軟件開發(fā)過程中的作用越來越受到軟件開發(fā)者的重視,確保軟件系統(tǒng)在任何時候都與需求規(guī)約一致,已經(jīng)成為軟件開發(fā)者及使用者關(guān)注的重要問題,利用場景對系統(tǒng)進行建模和分析已成為軟件開發(fā)過程中形式化驗證的重要技術(shù)和方法[1]。目前形式化驗證方法主要包括模型驗證[2]與運行時驗證[3]等。

    基于場景的形式化驗證經(jīng)常使用順序圖對系統(tǒng)進行建模和分析,順序圖是一種基于場景的語言,能夠圖形化地表示系統(tǒng)實例間交互的時序關(guān)系。順序圖包括消息順序圖(Message Sequence Chart,簡稱MSC)[4]、.0順序圖(UML2.0 Sequence Diagram,簡稱UML-SD)[5]、活性順序圖(Live Sequence Chart,簡稱LSC)[6]及其它變種。MSC由ITU提出并在業(yè)界得到廣泛應(yīng)用,但MSC表達能力很有限,只能表示可能發(fā)生的場景,不能表示系統(tǒng)必須滿足的場景。雖然UML-SD增加了一些新的操作符,增強了其表達能力,但UML-SD的非形式化語義也限制了其應(yīng)用。LSC對MSC進行擴展,LSC使用universal和existential兩種模式區(qū)分強制場景和可能場景,且LSC具有形式化語義。因此,軟件開發(fā)過程中形式化驗證經(jīng)常使用LSC描述系統(tǒng)場景中事件交互的時態(tài)關(guān)系。此外,LSC可以用來建模實際系統(tǒng),也可以用于描述場景需求,基于LSC的形式化驗證方法不僅使系統(tǒng)需求的行為語義易于理解,而且還能盡早地發(fā)現(xiàn)軟件設(shè)計錯誤。利用LSC對系統(tǒng)進行建模和分析已成為需求分析階段的重要技術(shù)和方法。

    LSC在MSC的基礎(chǔ)上增加了活性(liveness)的概念,活性表示需求的場景一定會發(fā)生[7]。LSC分為universal和existential兩種模式,universal圖表示系統(tǒng)一定發(fā)生的場景,用實線矩形框表示,existential圖表示系統(tǒng)可能發(fā)生的場景,用虛線矩形框表示。universal圖包含一個前置圖(prechart)和一個主圖(main chart),前置圖表示觸發(fā)場景,用虛線六邊形表示,主圖表示響應(yīng)場景,用實線矩形表示,universal圖表示的意思是,如果前置圖表示的觸發(fā)場景成功執(zhí)行了,主圖就必須執(zhí)行。existential圖則只含有主圖,不包含前置圖,existential圖只要求前置圖與主圖的一個事件實例,不強制要求主圖要在每一次前置圖執(zhí)行后執(zhí)行。

    圖1 universal模式LSC圖

    為了描述系統(tǒng)的強制性行為和可能性行為,LSC對圖中所有的位置、消息和條件等元素分配了溫度屬性,若元素的溫度是Hot,則該元素一定會發(fā)生,若元素的溫度值是Cold,則該元素可能會發(fā)生。在LSC圖中,Hot用實線表示,描述系統(tǒng)滿足強制行為;Cold用虛線表示,描述系統(tǒng)可能滿足的行為。如果實例線上某個位置是Hot位置,可以直接從當前位置移動到下一個Hot位置;如果這個位置是Cold位置,實例運行可能通過該位置。如果某個消息溫度值是Hot,則該消息一定會被發(fā)送與接收;如果消息的溫度值是Cold,表示該消息一定會被發(fā)送,但是消息可能被接收,也可能不被接收。

    1 LSC語言定義

    下面基于文獻[8]形式化定義LSC語言,首先定義LSC語法,由于基于LSC的形式化驗證過程一般基于程序執(zhí)行軌跡,這里給出LSC基于軌跡的語義。文獻[9]論述LSC具有很強的表達能力,為了充分使用LSC進行形式化驗證,有必要對LSC的復雜性進行論述。

    1.1LSC語法

    令inst(c)表示LSC圖c的實例線集合,dom(c,i)表示實例線i上的位置集合,dom(c)表示LSC圖c上位置集合。

    定義1(LSC):LSC定義為一個7元組L=<I,dom,ML,SR,Pre,Mode,quant>,其中:

    1)I是實例線的結(jié)合;

    2)Dom是圖c上的位置集合;

    3)ML是圖c的消息集合;

    4)SR是圖c的同步發(fā)生區(qū)域;

    5)Pre是圖c的前置圖,可為空。

    6)Mode∈{initial,invariant,iterative},Mode決定LSC的執(zhí)行頻率。

    7)quant∈{universal,existential},quant決定LSC的模式。

    1.2LSC基于軌跡的語義

    由于定義LSC基于軌跡的語義時要使用LSC的cut,這里首先定義LSC的cut。

    定義2(cut[8])一個cut指圖中每個實例到其位置的一個映射,cut?dom(c,i0)×...×dom(c,in),其中inst(c)={i0,...,in}。

    使用cut,下面定義LSC的執(zhí)行軌跡。

    定義3(執(zhí)行軌跡):令cuts序列c=c0,c1,...,ck為LSC圖c的一次執(zhí)行,執(zhí)行軌跡w=trace(c),則w=w0w1,...,wk。其中c0,wi表示圖c中事件的集合。

    一個LSC的軌跡語言是LSC圖c執(zhí)行所產(chǎn)生的所有執(zhí)行軌跡的集合。Lc={w|?(c0,c1,...ck)∈R uns(c)},使得w =trace(c0,c1,...,ck),其中Runs(c)表示LSC所有執(zhí)行軌跡的集合。

    1.3LSC語言的表達能力與復雜性論述

    在一定限制條件下,可以將LSC轉(zhuǎn)換為等價的時序邏輯語言或者自動機語言[9],這表明LSC語言具有很強的表達能力。Bontemps等人[10]主要討論了LSC語言的復雜性,表明LSC語言復雜性主要包括兩個方面:1)LSC語義依賴于偏序關(guān)系;2)LSC的規(guī)約是非結(jié)構(gòu)化的。前者引起的復雜性可以在實際應(yīng)用中避免,因為實際應(yīng)用場景一般是線性時序場景。后者引起的復雜性問題可以通過額外的信息生成高效的算法來解決。研究表明,LSC轉(zhuǎn)換為時序邏輯語言或自動機語言的復雜度相對較小,因此LSC經(jīng)常用于形式化驗證。

    2 基于LSC的形式化驗證方法

    在形式化驗證過程中,主要有建模系統(tǒng)和描述需求規(guī)約兩類需求。由于LSC可以用來建模系統(tǒng)行為,也可以用于描述場景需求[8]。因此,基于LSC的形式化驗證方法關(guān)鍵技術(shù)主要從以下兩個方面進行論述。

    2.1使用LSC建模系統(tǒng)行為

    形式化驗證需要建模系統(tǒng)行為,MSC可以直觀的描述系統(tǒng)中對象間的交互情景,MSC可以解決基于狀態(tài)圖作為系統(tǒng)行為模型的局限性問題,但是在捕獲系統(tǒng)行為需求時,MSC也存在一些不足[11],LSC也可以建模眾多系統(tǒng),且LSC語言可以補充MSC的不足,因此,使用LSC建模系統(tǒng)行為的研究逐漸展開。使用LSC建模系統(tǒng)行為即從基于場景規(guī)約的LSC構(gòu)建可執(zhí)行的系統(tǒng)。目前主要有兩種方法[12],第一種是自動合成系統(tǒng)的方法。給定LSC模型,確定是否存在一個系統(tǒng)滿足該LSC模型,如果存在這樣的系統(tǒng),則根據(jù)LSC模型中實例間的交互確定實例的有限狀態(tài)機或狀態(tài)圖,有限狀態(tài)機或狀態(tài)圖集合構(gòu)成確定滿足該LSC的系統(tǒng),但是合成的系統(tǒng)要滿足兩個需求:1)合成的系統(tǒng)需要監(jiān)聽系統(tǒng)中發(fā)生的事件;2)合成的系統(tǒng)必須滿足LSC模型,自動合成系統(tǒng)的方法已在文獻[11]實現(xiàn)。第二種方法是從LSC規(guī)約中場景實例間的交互建??蓤?zhí)行的系統(tǒng)[13],該方法不是為每個實例產(chǎn)生實例的內(nèi)部規(guī)約,而是按照算法直接執(zhí)行場景,在LSC的場景描述中定義可執(zhí)行的系統(tǒng)及系統(tǒng)運行產(chǎn)生的狀態(tài)。這種方法有一個研究成果,即Play-out機制[13],Play-out機制允許工程師與其它相關(guān)人員更好地了解場景實例交互所產(chǎn)生的行為。

    這兩種常見的方法各有特點,兩種方法的比較見表1所列。

    2.2使用LSC獲取待驗證的系統(tǒng)性質(zhì)

    形式化驗證經(jīng)常使用時序邏輯語言或自動機語言等描述系統(tǒng)的待驗證性質(zhì)。但在工程應(yīng)用中,尤其是在基于場景的軟件工程中使用時序邏輯并不實際。由于LSC語言具有直觀性和形式化的特點,因此在形式化驗證中,LSC經(jīng)常作為系統(tǒng)開發(fā)過程中需求規(guī)約描述語言,然后將LSC轉(zhuǎn)換為待驗證的性質(zhì),這些性質(zhì)然后用時序邏輯語言或自動機語言進行描述。關(guān)于從LSC獲取待驗證的系統(tǒng)性質(zhì),下面分LSC轉(zhuǎn)換為時序邏輯和LSC轉(zhuǎn)換為自動機兩種類型進行論述。

    表1 使用LSC建模系統(tǒng)的兩種方法比較

    2.2.1LSC轉(zhuǎn)換為時序邏輯

    Bontemps等人[14]對于只含LSC核心語法的LSC規(guī)約,證明任何LSC規(guī)約都可以轉(zhuǎn)換為時序邏輯公式。Kugler等人[15]設(shè)計算法將LSC轉(zhuǎn)換為LTL公式,其它相關(guān)的研究很多基于該轉(zhuǎn)換算法,文獻[15]主要產(chǎn)生兩種性質(zhì):圖中消息的偏序性質(zhì)(φ性質(zhì)),圖中消息的唯一性性質(zhì)(χ性質(zhì))。對于一個universal圖,對應(yīng)的LTL公式φc形式如下。

    該轉(zhuǎn)換等式從上到下分為三部分,頂部的φ性質(zhì)保證了前置圖與主圖中的消息都是偏序關(guān)系,中部保證了只有前置圖的消息都發(fā)生后,主圖中的消息才并且一定發(fā)生,底部保證了圖中的消息只發(fā)生一次。文獻[15]中的轉(zhuǎn)換方法為LSC圖每一個可能的執(zhí)行入口都生成LTL公式,轉(zhuǎn)換后的LTL公式的規(guī)模是LSC中事件規(guī)模的平方復雜度。Kumar等人[16]從化簡偏序性性質(zhì)和化簡唯一性性質(zhì)兩個方面,利用LSC規(guī)約中性質(zhì)的實現(xiàn)文獻[15]中轉(zhuǎn)換的優(yōu)化,優(yōu)化后所產(chǎn)生時序邏輯的規(guī)模是主圖中最大消息規(guī)模的平方復雜度,該優(yōu)化在大多數(shù)情況下可以縮小轉(zhuǎn)換所產(chǎn)生的LTL公式的規(guī)模。

    此外,LSC轉(zhuǎn)換為時序邏輯這些方法有一定的限制,這些方法的研究一般只針對LSC核心語法所表示的需求規(guī)約,缺少將完整LSC語法轉(zhuǎn)換為時序邏輯的算法。

    2.2.2LSC轉(zhuǎn)換為自動機

    文獻[17]實現(xiàn)了LSC轉(zhuǎn)換為自動機,他們將符號化自動機結(jié)構(gòu)形式的LSC圖作為輸入的自動機結(jié)構(gòu),然后通過增加接受狀態(tài)和增加/更新遷移將符號化自動機結(jié)構(gòu)轉(zhuǎn)換為可以檢測安全與活性錯誤的否定自動機。該轉(zhuǎn)換過程關(guān)注于創(chuàng)建自動機結(jié)構(gòu),并使用得出的自動機實現(xiàn)形式化驗證,如果需求規(guī)約用時間擴展的LSC表示,則可將LSC轉(zhuǎn)換為時間自動機。一般的轉(zhuǎn)換過程關(guān)注于創(chuàng)建自動機結(jié)構(gòu),Kumar等人[18]則直接研究了適用于發(fā)現(xiàn)系統(tǒng)錯誤的LSC到自動機的轉(zhuǎn)換過程,他們的LSC轉(zhuǎn)換為自動機的轉(zhuǎn)換過程使得性能與可擴展性均顯著提升。

    將LSC規(guī)約轉(zhuǎn)換為自動機語言,然后使用基于自動機語言進行形式化驗證,這種方法可以支持LSC的更大語法子集,且支持更大規(guī)模的LSC規(guī)約[17]。

    3 基于LSC的形式化驗證典型應(yīng)用

    基于LSC的形式化驗證應(yīng)用已有很多,從形式化驗證方法分類來看,目前基于LSC的形式化驗證主要應(yīng)用有模型驗證領(lǐng)域與運行時驗證領(lǐng)域等。下面就基于LSC的形式化驗證在模型驗證領(lǐng)域與運行時驗證領(lǐng)域的應(yīng)用進展加以論述。

    3.1基于LSC形式化方法的模型檢測

    LSC可以作為系統(tǒng)需求規(guī)約描述語言,通過將LSC轉(zhuǎn)換為時序邏輯語言或自動機語言的方法可以從LSC獲取系統(tǒng)待驗證的性質(zhì)[17]。此外,LSC又可以建模系統(tǒng)行為,因此,LSC也是系統(tǒng)的高級編程語言。模型檢測即需要建模系統(tǒng)也需要時序邏輯或自動機語言等表示的需求規(guī)約,而LSC正好具有上述兩種表述能力。因此,很多模型檢驗應(yīng)用研究都基于LSC,基于LSC形式化方法的模型檢驗應(yīng)用研究可以分為三類:

    1)LSC只轉(zhuǎn)化為系統(tǒng)行為模型,待驗證的系統(tǒng)性質(zhì)規(guī)約由用戶定義[17];

    2)系統(tǒng)行為模型由其它模型產(chǎn)生,待驗證系統(tǒng)性質(zhì)規(guī)約從LSC中獲?。?9];

    3)系統(tǒng)行為模型由LSC轉(zhuǎn)換形成,待驗證系統(tǒng)性質(zhì)規(guī)約也從LSC中獲?。?]。

    其中,情形3)的基于LSC形式化方法的模型檢測過程如圖2所示。

    圖2 基于LSC形式化方法的模型檢測過程

    3.2基于LSC形式化方法的運行時驗證

    LSC可以轉(zhuǎn)換為時序邏輯語言或者自動機語言來獲取系統(tǒng)需求規(guī)約,將轉(zhuǎn)換的時序邏輯語言或者自動機語言表示的需求規(guī)約作為監(jiān)控器[3],使用運行時驗證的相關(guān)技術(shù)[20]就可以實現(xiàn)基于LSC形式化方法的運行時驗證?;贚SC形式化方法的運行時驗證過程如圖3所示。

    圖3 基于LSC形式化方法的運行時驗證過程

    基于LSC的形式化方法應(yīng)用于運行時驗證領(lǐng)域已經(jīng)有相關(guān)研究,Chai等人[21]提出中標準LSC語言在其研究的嵌入式實時系統(tǒng)中表示特定場景的正確性性質(zhì)還不夠充分,因此引入充分前置圖的概念,提出擴展的活性順序圖 (extension of live sequence charts,簡稱eLSC),并分為有迭代eLSC和無迭代eLSC兩種場景,有迭代eLSC場景直接使用文獻[15]中的方法轉(zhuǎn)換成為LTL公式,并使用公式重寫的方法使用Maude工具引擎[22]進行運行時驗證,無迭代eLSC場景則設(shè)置專門的算法進行運行時驗證。并研究了歐洲列車控制系統(tǒng)(ETCS)中RBC/RBC切換場景,實現(xiàn)基于LSC形式化方法用于運行時驗證。

    4 基于LSC的驗證工具實現(xiàn)

    本文實現(xiàn)的基于LSC的驗證工具的設(shè)計思路是:首先,插裝獲取系統(tǒng)執(zhí)行軌跡,導入目標系統(tǒng)程序,使用Spring AOP進行代碼插裝獲取其執(zhí)行軌跡;然后,輸入使用從LSC轉(zhuǎn)換所得的LTL公式;最后,自動生成被驗證的項目文件,再調(diào)用Maude工具引擎實現(xiàn)運行時驗證。

    4.1工具架構(gòu)

    本文設(shè)計的基于LSC的驗證工具架構(gòu)如圖4所示。

    圖4 運行時驗證工具框架

    1)插裝獲取系統(tǒng)執(zhí)行軌跡:

    在此模塊中,用戶可以導入要驗證的目標系統(tǒng)源程序,并且可以在工具中查找已導入的目標系統(tǒng)程序代碼。在目標系統(tǒng)程序運行時,根據(jù)配置的插裝點通過Spring AOP插裝獲取目標系統(tǒng)的執(zhí)行軌跡序列,并將執(zhí)行軌跡序列存貯在本地,便于后續(xù)的運行時驗證。

    2)導入需求規(guī)約:

    在此模塊中,根據(jù)LSC描述的需求規(guī)約場景,用戶可以導入從LSC轉(zhuǎn)換所得的LTL公式,導入的LTL公式作為需求規(guī)約將存貯在本地,便于后續(xù)的運行時驗證。

    3)運行時驗證:

    在此模塊中,工具根據(jù)公式重寫算法自動生成相應(yīng)的重寫規(guī)則,Maude工具引擎根據(jù)重寫規(guī)則文件運行產(chǎn)生監(jiān)控器,監(jiān)控器分別根據(jù)(1)和(2)獲取的系統(tǒng)執(zhí)行軌跡和需求規(guī)約進行重寫邏輯的運行時驗證,并顯示驗證結(jié)果。

    4.2工具實現(xiàn)

    4.2.1插裝獲取系統(tǒng)執(zhí)行軌跡模塊實現(xiàn)

    該模塊的作用是通過Spring AOP插裝獲取目標系統(tǒng)的執(zhí)行軌跡。在該模塊中,GetSystem Trace類調(diào)用目標系統(tǒng)運行,RBC2RBCAspect類根據(jù)配置的插裝點進行代碼插裝,當目標系統(tǒng)運行完成后,RBC2RBCAspect類的通知代碼獲取系統(tǒng)的執(zhí)行軌跡序列。然后由GetSystem Trace類生成原子命題聲明文件與執(zhí)行軌跡序列日志文件。如圖5所示是本模塊的靜態(tài)結(jié)構(gòu)圖。

    圖5 插裝獲取系統(tǒng)執(zhí)行軌跡模塊靜態(tài)結(jié)構(gòu)圖

    4.2.2需求規(guī)約導入模塊實現(xiàn)

    該模塊的作用是導入從LSC轉(zhuǎn)換所得的LTL公式,同時生成相應(yīng)的需求規(guī)約文件并將其存儲在本地,生成的需求規(guī)約文件將作為需求規(guī)約輸入到Maude工具引擎中。如圖6所示是本模塊的靜態(tài)結(jié)構(gòu)圖。

    圖6 需求規(guī)約導入模塊靜態(tài)結(jié)構(gòu)圖

    4.2.3運行時驗證模塊實現(xiàn)

    該模塊的作用是調(diào)用Maude工具引擎進行運行時驗證。該模塊中,RunDemo類生成相應(yīng)的重寫規(guī)則,Maude工具引擎根據(jù)重寫規(guī)則文件進行運行時驗證,并顯示運行時驗證結(jié)果。如圖7所示是本模塊的靜態(tài)結(jié)構(gòu)圖。

    圖7 運行時驗證模塊的靜態(tài)結(jié)構(gòu)圖

    4.2.4驗證過程

    第一,插裝獲取系統(tǒng)執(zhí)行軌跡。首先,工具將導入并運行目標系統(tǒng),當目標系統(tǒng)運行結(jié)束后,工具就獲取了執(zhí)行軌跡序列。第二,導入待驗證的需求規(guī)約,輸入從LSC轉(zhuǎn)換所得的LTL公式形式的需求規(guī)約。最后,進行運行時驗證。工具首先生成重寫規(guī)則文件,然后調(diào)用Maude工具引擎,Maude工具引擎根據(jù)重寫規(guī)則產(chǎn)生預測監(jiān)控器,進行運行時驗證,并顯示驗證結(jié)果。本次實驗結(jié)果如圖8所示。

    本次實驗結(jié)果為“maybe”,由于從LSC轉(zhuǎn)換所得的LTL公式含有時序邏輯運算符G,驗證工具分析目前的執(zhí)行軌跡沒有發(fā)生需求違約,但對以后的執(zhí)行情況還無法確定,判定結(jié)果為可能為真,因此驗證結(jié)果為maybe,這也體現(xiàn)出LTL三值語義實現(xiàn)了對LTL二值語義的自然覆蓋。然后進行另一組實驗,本次插裝獲取另一條軌跡t=HOVCond,pre,req,ack,rri,使用工具進行運行時驗證,該執(zhí)行軌跡的實驗結(jié)果為“false”,如圖9所示。

    圖8 運行時驗證

    圖9 執(zhí)行軌跡違反規(guī)約的驗證結(jié)果

    5 結(jié)語

    基于LSC的形式化驗證方法已成為軟件開發(fā)過程中一種重要的驗證方法,基于LSC的形式化驗證已經(jīng)成功應(yīng)用到多個領(lǐng)域。本文對基于LSC的形式化驗證方法進行研究,論述LSC的理論基礎(chǔ),對比分析了基于LSC的形式化驗證領(lǐng)域的關(guān)鍵技術(shù)與應(yīng)用進展,并實現(xiàn)一種基于活性順序圖的驗證工具,實驗證明使用本驗證工具進行運行時驗證的可行性。隨著軟件規(guī)模不斷擴大系統(tǒng)集成度不斷提高,基于LSC的形式化驗證方法必將在軟件開發(fā)過程中發(fā)揮其應(yīng)有的價值。

    [1]Li X S,Liu Z M,He J F.A formal semantics of UML sequence diagram[A].Proceedings of the 2004 Australian Software Engineering Conference[C].2004:168-177.

    [2]Clarke E M,Grumberg O,Peled D A.Model Checking[M].MIT press,1999.

    [3]Leucker M,Schallhart C.A brief account of runtime verification[J].The Journal of Logic and Algebraic Programming,2009,78(5):293-303.

    [4]ITU-T.Recommendation Z.120:Message Sequence Charts[Z]. Geneva:ITU-T,1999.

    [5]Object Management Group (OMG).UML[Z]:Superstructure Version 2.2.2009.

    [6]Damm W,Harel D.LSCs:Breathing Life into Message Sequence Charts[J].Formal Methods in System Design,2001,19(1):45-80.

    [7]李雯睿,王志堅,張鵬程.模態(tài)順序圖u MSD的形式化語義[J].軟件學報,2011,22(4):659-675.

    [8]Larsen KG,Li S.Scenario-based analysis and synthesis of real-time systems using Uppaal[A].Proc13th Conference on Design,Automation,and Test in Europe[C].2010:447-452.

    [9]Harel D,Maoz S,Segall I.Some Results on the Expressive Power and Complexity of LSCs[J].In Pillars of computer science,2008,351-366.

    [10]Bontemps Y,Schobbens P.The Complexity of Live Sequence Charts[J].Institut d'Informatique,University of Namurrue Grandgagnage,21B5000-Namur(Belgium),2005,15.

    [11]Harel D,Segall I.Synthesis from scenario-based specifications[J].Journal of Computer and System Sciences,2012:78(3),970-980.

    [12]Harel D,Kantor A,Maoz S.On the Power of Play-Out for Scenario-Based Programs.[J].Lecture Notes in Computer Science,2010:207-220.

    [13]Brenner C,Greenyer J,Panzica V et al.The ScenarioTools Play-Out of Modal Sequence Diagram Specifications with Environment Assumptions[A].In Proc.12th Int Workshop on Graph Transformation and Visual Modeling Techniques.Volume 58,EASST [C].2013.

    [14]Bontemps Y,Schobbens P.The Computational Complexity of Scenario-based Agent Verification and Design[J].Journal of Applied Logic,2007,5(2):252-276.

    [15]Kugler H,Harel D,Pnueli A et al.Temporal logic for scenariobased specifications[A].Proc.of the 11th Int.Conf.on Tools and Algorithms for the Construction and Analysis of Systems(TACAS05)[C].2005:3440,445-460.

    [16]Kumar R,Mercer E,Bunker A.Improving translation of live sequence charts to temporal logic[A].Proc.of the 7th Int.Conf. on Automated Verification of Critical Systems(AVoCS07)[C]. 2007,183-197.

    [17]Kumar R,Eric G Mercer.Verifying Communication Protocols U-sing Live Sequence Chart Specifications[J].Electronic Notes in Theoretical Computer Science,2009,250(2):33-48.

    [18]Kumar R,Mercer EG.Improved live sequence chart to automata translation for verification[J].Electronic Communications of the EASST,Volume 10,2008.

    [19]Li SH,Balaguer S,David A,G.Larsen K,Nielsen B,Pusinskas S.Scenario-based verification of real-time systems using UPPAAL[C].Form Methods System Design,2010,37:200-264.

    [20]張碩,賀飛.運行時驗證技術(shù)的研究進展[J].計算機科學,2014,41(11A):359-363.

    [21]Chai M,Schlingloff B.Monitoring Systems with Extended Live Sequence Charts[J].Springer International Publishing Switzerland,RV 2014,LNCS 8734,48-63.

    [22]Clavel,Duran,Marti-Oliet,Meseguer,Talcott et al.Maude Manual[M] (version 2.6).University of Illinois,Urbana-Champaign,2011.

    Research on Formal Verification Method and Verification Tool Based on Live Sequence Chart

    Zhang Kun,Ye Junmin,Wang Qiang,Zhao Lixian,Chen Shu
    (School of Computer Science,Central China Normal University,Wuhan430079,China)

    In recent years,the role of formal verification technology in the software development process is growing more and more important.How to use formal verification technology to improve the reliability of software systems is a major concerned problem of software developers and users.This paper summarizes the progress of formal verification method based on Live Sequence Chart recently.In this paper,the language of live sequence chart,its expressive power and complexity are first introduced.Then the existing key technologies and their application of formal verification method based on live sequence chart are analyzed.Finally,the runtime verification tool based on live sequence chart is implemented,experiments show the feasibility of using this verification tool to formal verification.

    live sequence chart;formal verification;software development process

    1671-4598(2016)05-0274-05

    10.16526/j.cnki.11-4762/tp.2016.05.076

    TP393

    A

    2015-11-14;

    2015-12-15。

    國家科技支撐計劃項目(2015BAK33B00);教育部規(guī)劃基金項目(15YJA880095);中央高?;究蒲袠I(yè)務(wù)費專項資金科研項目(CCNU15GF003)。

    張坤(1992-),湖北武漢人,碩士研究生,主要從事軟件分析與驗證方向的研究。

    猜你喜歡
    自動機規(guī)約時序
    時序坐標
    基于Sentinel-2時序NDVI的麥冬識別研究
    {1,3,5}-{1,4,5}問題與鄰居自動機
    一種基于模糊細胞自動機的新型疏散模型
    智富時代(2019年4期)2019-06-01 07:35:00
    電力系統(tǒng)通信規(guī)約庫抽象設(shè)計與實現(xiàn)
    一種在復雜環(huán)境中支持容錯的高性能規(guī)約框架
    廣義標準自動機及其商自動機
    一種改進的LLL模糊度規(guī)約算法
    一種毫米波放大器時序直流電源的設(shè)計
    電子制作(2016年15期)2017-01-15 13:39:08
    修辭的敞開與遮蔽*——對公共話語規(guī)約意義的批判性解讀
    欧美成人免费av一区二区三区| 日日啪夜夜撸| 国产高清视频在线观看网站| 一级毛片我不卡| 欧美丝袜亚洲另类| 成人美女网站在线观看视频| h日本视频在线播放| 欧美+亚洲+日韩+国产| 国产精品,欧美在线| 日本免费a在线| 一进一出抽搐动态| 中文字幕久久专区| 国产精品综合久久久久久久免费| 国产一区二区在线av高清观看| 插阴视频在线观看视频| 老女人水多毛片| 国语自产精品视频在线第100页| 91av网一区二区| 国产一区二区三区在线臀色熟女| 最新在线观看一区二区三区| 亚洲欧美日韩东京热| 天天躁夜夜躁狠狠久久av| 久久人人爽人人爽人人片va| 国产成人aa在线观看| 人妻丰满熟妇av一区二区三区| 亚洲人成网站在线播放欧美日韩| 精品一区二区免费观看| 97热精品久久久久久| 亚洲美女搞黄在线观看 | 九色成人免费人妻av| 国产成人影院久久av| 亚洲国产精品国产精品| 永久网站在线| 亚洲精品粉嫩美女一区| 狂野欧美白嫩少妇大欣赏| 久久人妻av系列| 一个人看视频在线观看www免费| 男人舔奶头视频| 国产精品国产三级国产av玫瑰| 成人无遮挡网站| 亚洲精品乱码久久久v下载方式| 国内精品一区二区在线观看| 99久久精品热视频| 久久国内精品自在自线图片| 亚洲欧美日韩高清在线视频| 插逼视频在线观看| 欧美精品国产亚洲| 少妇人妻精品综合一区二区 | 精品少妇黑人巨大在线播放 | 12—13女人毛片做爰片一| 亚洲精品色激情综合| 午夜免费激情av| 中文字幕人妻熟人妻熟丝袜美| 日本成人三级电影网站| 91麻豆精品激情在线观看国产| 亚洲精品影视一区二区三区av| 内地一区二区视频在线| 免费无遮挡裸体视频| 3wmmmm亚洲av在线观看| 国产成人a∨麻豆精品| 精品久久久久久成人av| 亚洲电影在线观看av| 久久久久久久久大av| 一边摸一边抽搐一进一小说| 久久久久久久久久久丰满| 国语自产精品视频在线第100页| 色在线成人网| av卡一久久| 亚洲国产精品国产精品| 国产熟女欧美一区二区| 床上黄色一级片| 久久久国产成人免费| 日韩大尺度精品在线看网址| 久久久午夜欧美精品| 国产一区二区激情短视频| 亚洲人与动物交配视频| 人人妻人人看人人澡| 久久久午夜欧美精品| 成人漫画全彩无遮挡| 成人鲁丝片一二三区免费| 亚洲最大成人中文| 久久精品国产清高在天天线| 一本久久中文字幕| 看黄色毛片网站| 日日啪夜夜撸| 欧美成人a在线观看| 日韩欧美国产在线观看| 国产乱人视频| 久久6这里有精品| 蜜桃久久精品国产亚洲av| 三级经典国产精品| 久久久久久久久大av| 免费观看的影片在线观看| 日韩大尺度精品在线看网址| 亚洲成人精品中文字幕电影| 日本a在线网址| 一卡2卡三卡四卡精品乱码亚洲| 少妇高潮的动态图| 在线免费观看的www视频| 国产精品嫩草影院av在线观看| 亚洲三级黄色毛片| 日韩欧美精品v在线| 一区二区三区四区激情视频 | 小说图片视频综合网站| 国产成年人精品一区二区| 99在线视频只有这里精品首页| 成人一区二区视频在线观看| 久久国产乱子免费精品| 国产精华一区二区三区| 中国美白少妇内射xxxbb| 无遮挡黄片免费观看| 一区二区三区四区激情视频 | 夜夜看夜夜爽夜夜摸| 天堂动漫精品| 国产69精品久久久久777片| 国产免费男女视频| 一区福利在线观看| 日韩欧美精品免费久久| 中文字幕av在线有码专区| 自拍偷自拍亚洲精品老妇| av视频在线观看入口| 色尼玛亚洲综合影院| 欧美三级亚洲精品| 久久综合国产亚洲精品| 丝袜喷水一区| 亚洲美女黄片视频| 超碰av人人做人人爽久久| 午夜福利成人在线免费观看| 亚洲成人久久性| 97在线视频观看| 韩国av在线不卡| 18+在线观看网站| 亚洲成人中文字幕在线播放| 亚洲四区av| 赤兔流量卡办理| 成人三级黄色视频| 男人和女人高潮做爰伦理| 日韩欧美在线乱码| 一进一出好大好爽视频| 日本一二三区视频观看| 午夜免费男女啪啪视频观看 | 高清毛片免费看| 免费一级毛片在线播放高清视频| 18禁黄网站禁片免费观看直播| 草草在线视频免费看| 少妇猛男粗大的猛烈进出视频 | 三级国产精品欧美在线观看| 久久6这里有精品| 国产高清三级在线| 亚洲欧美日韩无卡精品| 亚洲四区av| 国产精品不卡视频一区二区| 91麻豆精品激情在线观看国产| 老司机影院成人| 免费一级毛片在线播放高清视频| 搡女人真爽免费视频火全软件 | 三级经典国产精品| or卡值多少钱| 久久人妻av系列| 国产精品久久久久久亚洲av鲁大| av卡一久久| 国产探花在线观看一区二区| 日韩精品有码人妻一区| 国产黄色视频一区二区在线观看 | 淫妇啪啪啪对白视频| 22中文网久久字幕| 日韩欧美免费精品| 精品无人区乱码1区二区| 午夜日韩欧美国产| 97人妻精品一区二区三区麻豆| 中文字幕熟女人妻在线| 免费在线观看成人毛片| 天堂av国产一区二区熟女人妻| 精品熟女少妇av免费看| 香蕉av资源在线| 精品久久久久久久末码| 国产成人a∨麻豆精品| 直男gayav资源| 国产白丝娇喘喷水9色精品| 91av网一区二区| 久久韩国三级中文字幕| 亚洲图色成人| 国产精品一区二区三区四区免费观看 | 亚洲精品日韩av片在线观看| 露出奶头的视频| 日韩亚洲欧美综合| 又黄又爽又刺激的免费视频.| 久久鲁丝午夜福利片| 2021天堂中文幕一二区在线观| 久久久久久久午夜电影| 久久久色成人| 乱码一卡2卡4卡精品| 精品福利观看| 亚洲欧美成人综合另类久久久 | 有码 亚洲区| 成熟少妇高潮喷水视频| 日韩一本色道免费dvd| 亚洲aⅴ乱码一区二区在线播放| 午夜精品一区二区三区免费看| 色在线成人网| 国产精品美女特级片免费视频播放器| 国产高清不卡午夜福利| 亚洲av第一区精品v没综合| 日本一本二区三区精品| 国产一区二区三区av在线 | 淫妇啪啪啪对白视频| 亚洲欧美日韩无卡精品| 最近的中文字幕免费完整| 亚洲色图av天堂| 国产一区二区在线av高清观看| 亚洲精华国产精华液的使用体验 | 久久精品国产清高在天天线| 欧美zozozo另类| 国产精品伦人一区二区| 久久久久国产精品人妻aⅴ院| 五月伊人婷婷丁香| 一个人免费在线观看电影| 亚洲一区高清亚洲精品| 国产精品人妻久久久久久| 亚洲电影在线观看av| 久久精品国产清高在天天线| 69av精品久久久久久| 亚洲aⅴ乱码一区二区在线播放| 麻豆精品久久久久久蜜桃| 在线播放无遮挡| 99国产极品粉嫩在线观看| 嫩草影院精品99| 夜夜看夜夜爽夜夜摸| 日韩人妻高清精品专区| av免费在线看不卡| 国产精品精品国产色婷婷| 欧美成人a在线观看| 国产亚洲av嫩草精品影院| 久久久国产成人精品二区| 又黄又爽又刺激的免费视频.| 日韩,欧美,国产一区二区三区 | 五月玫瑰六月丁香| 男女边吃奶边做爰视频| 亚洲内射少妇av| 最近2019中文字幕mv第一页| 中文字幕久久专区| 91午夜精品亚洲一区二区三区| 黄色视频,在线免费观看| 男女视频在线观看网站免费| 久久久国产成人精品二区| 国产熟女欧美一区二区| 黑人高潮一二区| 国模一区二区三区四区视频| 免费黄网站久久成人精品| 成人精品一区二区免费| 最新中文字幕久久久久| 寂寞人妻少妇视频99o| 中国美女看黄片| 校园春色视频在线观看| 极品教师在线视频| 插逼视频在线观看| 99九九线精品视频在线观看视频| 亚洲一区高清亚洲精品| 国产精品一区二区三区四区免费观看 | 九色成人免费人妻av| 国产精品人妻久久久影院| 久久人人爽人人片av| 九九在线视频观看精品| 最近中文字幕高清免费大全6| 久久久精品大字幕| 深夜a级毛片| 国产精品嫩草影院av在线观看| 久久精品国产亚洲av涩爱 | 欧美激情在线99| 国产欧美日韩精品一区二区| 精品乱码久久久久久99久播| 午夜精品国产一区二区电影 | 五月伊人婷婷丁香| 国产成人aa在线观看| 免费av不卡在线播放| 我要看日韩黄色一级片| 国产探花在线观看一区二区| av免费在线看不卡| 欧洲精品卡2卡3卡4卡5卡区| 无遮挡黄片免费观看| 麻豆国产av国片精品| 久久久久久久久久成人| 综合色av麻豆| 又爽又黄a免费视频| 亚洲真实伦在线观看| 欧美在线一区亚洲| 国产免费男女视频| a级毛片免费高清观看在线播放| 国产在视频线在精品| 精品人妻视频免费看| 久久久国产成人免费| 成年版毛片免费区| 日本爱情动作片www.在线观看 | 日韩成人av中文字幕在线观看 | 校园人妻丝袜中文字幕| 久久久精品大字幕| 婷婷色综合大香蕉| 免费看av在线观看网站| av天堂在线播放| 亚洲欧美日韩高清专用| av.在线天堂| 69av精品久久久久久| 亚洲精华国产精华液的使用体验 | 少妇猛男粗大的猛烈进出视频 | 少妇的逼好多水| 亚洲熟妇中文字幕五十中出| 亚洲七黄色美女视频| 1024手机看黄色片| 欧美另类亚洲清纯唯美| 亚洲av成人精品一区久久| 国产精品人妻久久久久久| 精品一区二区三区人妻视频| 黑人高潮一二区| 亚洲最大成人手机在线| 天堂影院成人在线观看| 久久精品夜夜夜夜夜久久蜜豆| aaaaa片日本免费| 国产一级毛片七仙女欲春2| 色播亚洲综合网| 国产午夜精品论理片| 精品久久久久久久久av| 精品久久久噜噜| 一区福利在线观看| 性欧美人与动物交配| 国内少妇人妻偷人精品xxx网站| 最近手机中文字幕大全| 国产精品亚洲一级av第二区| 欧美成人一区二区免费高清观看| 一个人看的www免费观看视频| 欧美日韩乱码在线| 一个人看视频在线观看www免费| 国产国拍精品亚洲av在线观看| 在线播放国产精品三级| 九九久久精品国产亚洲av麻豆| 中出人妻视频一区二区| 91av网一区二区| 麻豆精品久久久久久蜜桃| 欧美一区二区精品小视频在线| 国产精华一区二区三区| 日本黄色视频三级网站网址| 久久九九热精品免费| 变态另类成人亚洲欧美熟女| 国产精品久久视频播放| 欧美最新免费一区二区三区| 精品久久久久久久末码| 人人妻人人澡人人爽人人夜夜 | 看黄色毛片网站| 国产av不卡久久| 丝袜喷水一区| 深夜精品福利| 精品久久久噜噜| 国产高清视频在线观看网站| 精品国内亚洲2022精品成人| 亚洲内射少妇av| 久久久久久久亚洲中文字幕| 亚洲av成人av| 联通29元200g的流量卡| 麻豆国产97在线/欧美| 联通29元200g的流量卡| 久久久久久久午夜电影| 赤兔流量卡办理| 有码 亚洲区| 午夜精品一区二区三区免费看| 久久久久久久久久黄片| 精品久久久噜噜| 五月玫瑰六月丁香| 一级毛片aaaaaa免费看小| 欧美精品国产亚洲| 精品国内亚洲2022精品成人| 久久久久久久午夜电影| 中文资源天堂在线| 免费看美女性在线毛片视频| 不卡视频在线观看欧美| 日本爱情动作片www.在线观看 | 国产亚洲精品久久久com| 亚洲中文字幕日韩| 精品欧美国产一区二区三| 国产精品久久久久久久电影| 国产精华一区二区三区| 12—13女人毛片做爰片一| 亚洲欧美日韩高清专用| 男女啪啪激烈高潮av片| 久久人人爽人人片av| 蜜臀久久99精品久久宅男| 久久精品国产亚洲网站| 亚洲美女黄片视频| 亚洲精品456在线播放app| 精品人妻视频免费看| 国产精品久久久久久久久免| 国产精品av视频在线免费观看| 亚洲av不卡在线观看| av国产免费在线观看| 人妻久久中文字幕网| 欧美bdsm另类| 亚洲第一电影网av| 亚洲av免费在线观看| 亚洲av成人精品一区久久| 国产男人的电影天堂91| 可以在线观看毛片的网站| 国产黄a三级三级三级人| 美女被艹到高潮喷水动态| 色综合站精品国产| 中文资源天堂在线| 成人午夜高清在线视频| av天堂中文字幕网| 国产亚洲av嫩草精品影院| 亚洲电影在线观看av| 午夜福利视频1000在线观看| 日韩欧美 国产精品| 在线免费十八禁| 久久热精品热| 女人被狂操c到高潮| 少妇人妻一区二区三区视频| 校园春色视频在线观看| 色吧在线观看| 99精品在免费线老司机午夜| 日韩强制内射视频| 两性午夜刺激爽爽歪歪视频在线观看| 天天躁日日操中文字幕| 午夜福利在线观看免费完整高清在 | 51国产日韩欧美| 日韩av不卡免费在线播放| 久久人人爽人人片av| 亚洲欧美日韩无卡精品| 精品99又大又爽又粗少妇毛片| 草草在线视频免费看| 亚洲第一电影网av| 天堂√8在线中文| 国产伦精品一区二区三区四那| 综合色av麻豆| 看免费成人av毛片| 高清毛片免费观看视频网站| 国产高潮美女av| 最近2019中文字幕mv第一页| 村上凉子中文字幕在线| 久久精品国产亚洲av天美| 久久精品国产清高在天天线| 免费观看精品视频网站| 激情 狠狠 欧美| 国产免费男女视频| 国模一区二区三区四区视频| 精品一区二区三区人妻视频| aaaaa片日本免费| 18禁黄网站禁片免费观看直播| 亚洲不卡免费看| 丰满的人妻完整版| 日韩大尺度精品在线看网址| 淫秽高清视频在线观看| 久久久久国产精品人妻aⅴ院| 嫩草影院入口| 不卡一级毛片| 99热全是精品| 在线观看一区二区三区| 亚洲在线自拍视频| 国产一区二区三区在线臀色熟女| 人妻制服诱惑在线中文字幕| videossex国产| 身体一侧抽搐| 在线看三级毛片| 午夜影院日韩av| 中文字幕免费在线视频6| 国产精品久久久久久精品电影| 午夜精品一区二区三区免费看| a级毛片a级免费在线| 久久精品国产亚洲av涩爱 | 观看免费一级毛片| 欧美一区二区国产精品久久精品| 成人永久免费在线观看视频| 久久天躁狠狠躁夜夜2o2o| 欧美日韩一区二区视频在线观看视频在线 | 69av精品久久久久久| 成人特级黄色片久久久久久久| 亚洲乱码一区二区免费版| 中文字幕精品亚洲无线码一区| 精品人妻偷拍中文字幕| 别揉我奶头~嗯~啊~动态视频| 国产极品精品免费视频能看的| 欧美成人a在线观看| 久久久久久久久久成人| 校园人妻丝袜中文字幕| 国产伦在线观看视频一区| 国产精品日韩av在线免费观看| 成人美女网站在线观看视频| 久久精品国产亚洲av香蕉五月| 亚洲美女搞黄在线观看 | 日本黄色片子视频| 免费看a级黄色片| 亚洲国产精品成人久久小说 | 亚洲专区国产一区二区| 日本爱情动作片www.在线观看 | 美女xxoo啪啪120秒动态图| 欧美潮喷喷水| 波多野结衣高清作品| 久久久a久久爽久久v久久| 99久久中文字幕三级久久日本| 高清毛片免费看| 热99在线观看视频| 国产伦精品一区二区三区四那| 国产黄色小视频在线观看| 在线观看免费视频日本深夜| 午夜激情欧美在线| 国产高清激情床上av| 中文字幕久久专区| 日韩欧美免费精品| 在线天堂最新版资源| 久久人人爽人人片av| 国产高清激情床上av| 成人欧美大片| 69av精品久久久久久| 免费在线观看影片大全网站| 如何舔出高潮| 久久人人爽人人爽人人片va| 国产探花极品一区二区| 日本一二三区视频观看| 人人妻人人澡欧美一区二区| 又爽又黄a免费视频| 亚洲精品国产成人久久av| 国语自产精品视频在线第100页| 99久国产av精品国产电影| 色在线成人网| 国产综合懂色| 乱人视频在线观看| 亚洲成人av在线免费| 国产麻豆成人av免费视频| 日韩精品有码人妻一区| 成人欧美大片| 国产成人a∨麻豆精品| 22中文网久久字幕| 成人亚洲精品av一区二区| 波多野结衣高清作品| 国产成人freesex在线 | 精品人妻视频免费看| 亚洲人成网站高清观看| 嫩草影院新地址| 色哟哟哟哟哟哟| 成年女人毛片免费观看观看9| 久久久久久久久久黄片| 内射极品少妇av片p| 久久午夜亚洲精品久久| 五月伊人婷婷丁香| 免费人成在线观看视频色| 亚洲七黄色美女视频| 12—13女人毛片做爰片一| 欧美另类亚洲清纯唯美| 一级毛片电影观看 | 天堂影院成人在线观看| 最近视频中文字幕2019在线8| 免费av不卡在线播放| 在线免费观看不下载黄p国产| 亚洲欧美成人综合另类久久久 | 又黄又爽又刺激的免费视频.| 亚洲av一区综合| 成年女人看的毛片在线观看| 男人狂女人下面高潮的视频| 国产高清视频在线观看网站| 特级一级黄色大片| 一本一本综合久久| 精品久久久久久久久亚洲| 欧美一级a爱片免费观看看| 91在线精品国自产拍蜜月| 国产成人精品久久久久久| 女人被狂操c到高潮| 亚洲熟妇中文字幕五十中出| 两性午夜刺激爽爽歪歪视频在线观看| 国产片特级美女逼逼视频| 亚洲精品日韩av片在线观看| 啦啦啦韩国在线观看视频| 亚洲av熟女| 在线观看av片永久免费下载| 在线播放国产精品三级| 国产精品女同一区二区软件| 免费观看在线日韩| 成熟少妇高潮喷水视频| 久久久久久国产a免费观看| 婷婷精品国产亚洲av| 麻豆乱淫一区二区| av免费在线看不卡| 日本熟妇午夜| 乱系列少妇在线播放| 亚洲美女视频黄频| 国产亚洲精品av在线| 男人的好看免费观看在线视频| 国产一区二区三区av在线 | 中文字幕av成人在线电影| 久久久久久久久久久丰满| 亚洲性夜色夜夜综合| 成人特级黄色片久久久久久久| 国产v大片淫在线免费观看| 国产黄a三级三级三级人| 在线观看66精品国产| 日本黄色片子视频| 亚洲内射少妇av| 亚洲成人av在线免费| 久久精品国产99精品国产亚洲性色| 亚洲内射少妇av| 精品不卡国产一区二区三区| 干丝袜人妻中文字幕| 国产欧美日韩精品亚洲av| 国产黄片美女视频| 97超级碰碰碰精品色视频在线观看| 国产高清视频在线观看网站| 三级经典国产精品| 国产视频内射| 国产亚洲91精品色在线| 亚洲专区国产一区二区| 成人二区视频| 国产一区二区激情短视频| 插逼视频在线观看| 人妻久久中文字幕网| 国产一区二区三区在线臀色熟女| 不卡一级毛片| 国产精品永久免费网站| 亚洲av一区综合| 中文字幕av成人在线电影| 久久久a久久爽久久v久久|