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

    基于NuSMV的AADL模型形式化驗證技術

    2022-04-26 02:13:46劉暢蔣永平馬春燕張濤
    航空學報 2022年3期
    關鍵詞:線程進程實例

    劉暢,蔣永平,馬春燕,*,張濤

    1.中國航空無線電電子研究所,上海 200233 2.西北工業(yè)大學 軟件學院,西安 710072

    為保障任務關鍵系統(tǒng)的高可靠性需求,在軟件系統(tǒng)的設計階段對任務關鍵屬性進行形式化驗證是有效的技術手段之一。

    AADL(Architecture Analysis and Design Language)是一種描述嵌入式系統(tǒng)架構的建模語言,在航空航天領域廣泛被應用。為在任務關鍵系統(tǒng)模型設計的早期階段,對AADL模型的任務關鍵屬性和系統(tǒng)行為的正確性進行驗證,NuSMV(New Symbolic Model Verifier)形式化模型發(fā)揮著重要的作用,NuSMV使用有限狀態(tài)機描述NuSMV模型,使用時態(tài)邏輯公式描述待驗證屬性,對相關屬性進行驗證。由于NuSMV工具的輸入語言支持以模塊化分層方式構建的復雜而龐大的系統(tǒng),與AADL的層次化方式建立系統(tǒng)模型的思想一致。因此,可以通過將AADL模型轉換為NuSMV形式化模型,完成AADL模型的形式化驗證,如果驗證失敗,NuSMV會給出反例路徑,方便模型驗證人員快速定位問題來源,對模型進行優(yōu)化。

    目前已有多項研究將AADL模型轉化為形式化語言描述的模型,如LNT、Event-B、BIP、Maude、TASM及CSP等,然后對AADL模型的相關建模屬性進行正確性驗證。然而,這些工作僅考慮一個小的AADL子集,未涵蓋全部AADL軟構件以及相關行為、配置相關的建模要素,而這些關鍵的建模元素在模型的正確性驗證中較為常見。本文擬采用NuSMV對AADL模型的安全性和活性等屬性進行驗證。

    1 相關工作

    Mkaouar等介紹了一種AADL模型子集到LNT的轉換方法,通過CADP工具對系統(tǒng)并發(fā)正確性進行驗證。文獻[6]使用Event-B對AADL模型架構進行形式化驗證,但不包括行為模型的屬性驗證。本文研究團隊豐富了AADL行為模型及可調度性等驗證內容,采用Event-B對AADL模型進行形式化驗證。

    Yang等將AADL轉換為抽象實時狀態(tài)機TASM,并基于定理證明器(Coq)對轉換的語義一致性進行驗證。劉倩等基于UPPAAL工具,對AADL模型可調度性進行分析,但其時間自動機模型不提供對時鐘的暫停及恢復,存在一定局限性。

    Yang等使用可達自動機CSP構建AADL的形式化語義,并且使用FDR工具驗證死鎖和活鎖。文獻[13]使用HCSP構建AADL子集的形式化語義,并通過定理證明的方法驗證AADL模型行為附件的正確性。Zhang等介紹了一種從AADL模型到CSP的映射規(guī)則,并使用PAT(Process Analysis Toolkit)驗證AADL的安全性、活性等任務關鍵屬性。

    文獻[15]將AADL轉換為NPTA(Networks of Priced Timed Automata)并且基于UPPAAL-SMC提出系統(tǒng)性能定性評估的方法。文獻[16]將AADL模型轉換為SIGNAL模型,并提供多時鐘約束的調度性分析。文獻[17]提出了利用NuSMV對AADL模型進行驗證的思想,但缺乏AADL模型到NuSMV模型的映射規(guī)則,以及采用NuSMV對AADL模型進行形式化驗證的系統(tǒng)化方法,僅通過一個案例說明如何利用NuSMV對AADL模型進行驗證。

    對以上研究工作進行總結,可以發(fā)現(xiàn)前人方法存在以下3點不足。

    1)部分研究工作考慮的AADL模型要素比較少,這樣會導致無法描述比較復雜的系統(tǒng)。

    2)大部分研究工作沒有證明其方法的正確性,無法保證形式化模型與源模型語義一致。

    3)模型系統(tǒng)待驗證屬性比較單一,局限性比較大。例如只支持LTL(Linear Temporal Logic)規(guī)范,這樣無法描述包含全稱和存在量詞的屬性。

    為了彌補這些缺點,本文提出基于NuSMV的AADL模型驗證方法。

    2 AADL和NuSMV

    AADL是系統(tǒng)架構分析和設計語言,提供了系統(tǒng)和軟硬件構件以及構件之間交互關系的建模要素,AADL模型可以作為航空嵌入式系統(tǒng)的設計模型。AADL的軟件構件包含系統(tǒng)、子系統(tǒng)、進程、線程、線程組、數(shù)據(jù)和子程序,每個軟件構件都由類型和實現(xiàn)構成。AADL系統(tǒng)構件或軟件構件的任務級模態(tài)是其所包含的構件、連接和屬性值關聯(lián)的顯式配置,代表系統(tǒng)或軟件構件可選的操作狀態(tài)模態(tài),模態(tài)配置也可以指定線程或子程序中要使用的不同調用序列,還可以表示在不同屬性值下的軟件構件(例如線程或子程序)的不同行為。系統(tǒng)或軟件構件行為的描述通過AADL行為附件(Behavior Annex)進行建模,例如描述構件的子程序調用、異步和時序等行為。

    NuSMV是一套基于符號模型檢測技術的形式化建模語言和工具,用于有限狀態(tài)系統(tǒng)的形式化驗證,可以用于分析計算樹邏輯(CTL)和線性時序邏輯(LTL)表示的屬性,例如,安全性屬性和活性屬性。NuSMV程序由模塊(MODULE)構成,模塊定義由形參(Paramenter)和主體(Body)組成。模塊主體由描述狀態(tài)集Variables、轉移關系和對模型的一些約束Constraint、待驗證的規(guī)范Specification組成。

    3 AADL模型到NuSMV模型的轉換方法

    AADL模型到NuSMV模型的轉換方法的研究分為2個階段:確定需要轉換的AADL子集;建立從AADL模型子集到NuSMV模型子集的映射規(guī)則。

    3.1 需要轉換的AADL子集

    本文只考慮AADL模型的軟件構件(數(shù)據(jù)、子程序、線程、進程)和系統(tǒng)構件5種構件類型(component_type),如表1所示。

    圖1采用類圖展示了需要轉換的AADL模型建模要素及AADL構件的包含關系,系統(tǒng)構件可以包含系統(tǒng)構件、進程構件、子程序構件和數(shù)據(jù)構件,進程構件可以包含線程構件和數(shù)據(jù)構件,線程構件可以包含子程序構件和數(shù)據(jù)構件,子程序構件可以包含數(shù)據(jù)構件。表1中構件類型和構件子元素類型在圖1中用類名表示,構件子元素類型的構成要素用類的屬性表示。

    表1 需要轉換的AADL子集Table 1 Subsets of AADL to be transformed

    圖1 需要轉換的AADL建模要素Fig.1 AADL modeling elements needed to be con-verted

    3.2 AADL模型到NuSMV模型的映射規(guī)則

    映射規(guī)則是基于AADL元模型和NuSMV元模型提出來的。為了保證映射規(guī)則的完整性、以及一致性,每條映射規(guī)則都滿足從AADL元模型到NuSMV元模型節(jié)點的一對一映射,即每條映射規(guī)則都是同構映射。本節(jié)描述了AADL模型構件到NuSMV模塊的7類映射規(guī)則,分別對應構件類型及構件包含的6類子元素到NuSMV模型的映射規(guī)則。

    圖2用UML類圖表示映射得到的NuSMV模型。AADL中的system、process、thread、subprogram和data構件分別映射為NuSMV中MODULE_main、MODULE_process、MODULE_thread、MODULE_subprogram和MODULE_data等5種類型的模塊(MODULE),這些模塊均繼承MODULE_component,除了MODULE_data,其余4種模塊屬性一致,均包括多個MODULE_feature實例、多個MODULE_connection實例、一個枚舉類型的modes變量、多個枚舉類型的flow變量。NuSMV程序以main模塊作為驗證入口,main模塊對應AADL模型中的系統(tǒng)根節(jié)點。AADL構件的模態(tài)(modes)、數(shù)據(jù)流(flows)可以用NuSMV中的基本數(shù)據(jù)類型表示。

    對本文提出的7類映射規(guī)則進行詳細闡釋,并結合算法1中的AADL進程構件MissionLoadP及其映射的NuSMV模塊為案例進行說明。

    圖2 映射得到的NuSMV模型Fig.2 NuSMV model obtained by mapping

    3.2.1 映射規(guī)則Rule1

    Rule1表示根據(jù)AADL構件A的類型,將構件映射為NuSMV模塊A。如果構件A為系統(tǒng)構件,則映射為圖2中的main模塊(MODULE_main);如果構件A為進程構件,則映射為MODULE_process,其他構件類型同理。圖3中的MissionLoadP進程構件映射為MissionLoadP模塊。

    1) 進程模塊中的布爾變量isActive標記其在系統(tǒng)模態(tài)下是否有效。

    2) 線程模塊中的布爾變量isBehavior標記線程組件在當前進程模態(tài)下是否執(zhí)行其行為。

    3) 進程模塊isActive變量的值隨著系統(tǒng)模塊模態(tài)切換而變換。線程模塊的isBehavior變量的值隨著進程模塊的模態(tài)切換而變換。

    3.2.2 映射規(guī)則Rule2

    構件A的features在表1中表示feature的集合。該集合中的每一個feature映射為一個feature MODULE實例,該實例會被connection模塊實例引用。特征模塊的定義如下:

    MODULE feature(feaType,feaDirec)

    DEFINE

    Type:= feaType;

    Direc:= feaDirec;

    1) feaType 代表特征類型,AADL中定義的特征類型有抽象特征(Feature)、端口特征(Port)、參數(shù)特征(Parameter)、數(shù)據(jù)構件訪問特征(Data Access)。在轉換后的NuSMV模型中分別用1代表抽象特征(Feature),2代表數(shù)據(jù)端口特征(Data Port),3代表事件端口特征(Event Port),4代表事件數(shù)據(jù)端口特征(Event Data Port),5代表參數(shù)特征(Parameter),6代表數(shù)據(jù)訪問特征(Data Access)。

    算法1 AADL進程構件及其映射的NuSMV模塊

    圖3 元模型和模型實例之間的映射關系Fig.3 Mappings between metamodels and models

    2) feaDirec 代表特征方向,AADL中定義的特征方向有輸入(in)、輸出(out)、輸入輸出(in out)、提供(provides)、請求(requires)。本文在轉換之后的NuSMV模型中用-1代表輸入(in)、1代表輸出(out)、0代表輸入輸出(in out)、-2代表請求(requires),2代表提供(provides)。

    3) 如果構件的特征接口為事件端口特征(event port)或事件數(shù)據(jù)端口特征(event data port),除了映射特征模塊實例,還需要在映射后的模塊中定義布爾類型變量,表示對應端口上的事件是否發(fā)生,該變量為TRUE代表事件到達,為FALSE代表事件未到達。該布爾類型變量可以作為模態(tài)轉換或行為狀態(tài)轉換的條件。

    算法1中MissionLoadP進程特征“reqDispandControl: in event port”映射為MODULE MissionLoadP中的“reqDispandControl:feature(3,-1)”。

    3.2.3 映射規(guī)則Rule3

    每個子構件映射為一個MODULE實例,所有子構件映射的MODULE實例均會被MODULE A引用。如果subcomponent_name是AADL構件A的某一個子構件的名字,component_type是子構件的類型,則映射的MODULE實例名為subcomponent_name,映射的MODULE實例的類型為component_type。

    算法1中的MissionLoadP進程構件包含線程子構件getLocalPlaneAttributeInfo。線程子構件在模塊MissionLoadP中表示為getInfo: getLocalPlaneAttributeInfo()。

    3.2.4 映射規(guī)則Rule4

    構件A的connections在表1中表示connection的集合,該集合中的每一條connection映射為connection MODULE實例。該實例會被模塊A引用,連接模塊的定義如下:

    MODULE connection(src_feature,dst_feature,conn_type)

    VAR

    isWorking: boolean;

    1) src_feature 對應連接的源特征,其類型為特征模塊(即MODULE_feature)。

    2) dst_feature 代表連接的目的特征,其類型為特征模塊(即MODULE_feature)。

    3) connType 代表連接類型,分為同級構件相連的連接類型、構件到子構件的連接類型及構件到父構件的連接類型,本文在NuSMV中分別用0、-1、1表示。

    4) isWorking用以驗證該連接在的模態(tài)下是否有效,其默認值為TRUE。

    算法1中的“conn1:port getInfo.outport→returnPlaneInfo”映射為“conn1:connection(getInfo.outport,returnPlaneInfo,1)”,getInfo.outport為源特征,returnPlaneInfo為目的特征,1表示構件MissionLoadP的子構件端口到該構件端口的連接。

    3.2.5 映射規(guī)則Rule5

    構件A的modes在表1中表示modes子元素類型,其映射為枚舉類型的modes變量,例如,該枚舉變量表示為modes:{mode1, mode2, mode3},其中,mode1、mode2、mode3對應表1中modes子元素類型的構成要素modes_set。算法1中的進程MissionLoadP的modes的轉換,枚舉值對應構件所有的操作狀態(tài),模態(tài)之間的轉移關系用NuSMV中的next()表達式和case語句表示。

    3.2.6 映射規(guī)則Rule6

    構件A的behavior_annex在表1中表示behavior_annex子元素類型,映射為一個behavior MODULE實例,例如算法1中的線程getLocalPlaneAttributeInfo 行為附件的轉換滿足以下映射規(guī)則:

    1)行為附件中的變量(variables)轉換為NuSMV模塊中的變量聲明。

    2)行為附件的狀態(tài)集合(states)轉換為NuSMV模塊中枚舉類型的變量聲明。NuSMV模塊中states變量的枚舉值對應行為附件中定義的狀態(tài),包括initial狀態(tài)、complete狀態(tài)、final狀態(tài)和execution狀態(tài)。

    3)行為附件中的復合狀態(tài)被分解為多個原子狀態(tài)。比如s0為initial和complete的一個復合狀態(tài),轉換成s0_initial和s0_complete 2個狀態(tài)。

    4)行為附件的轉移關系(transitions)映射為NuSMV的next(states)函數(shù)和case語句,描述AADL行為中行為狀態(tài)的轉移關系。

    3.2.7 映射規(guī)則Rule7

    構件A的flows在表1中表示flow的集合,該集合中的每一個flow映射為一個枚舉類型變量,例如AADL中flow映射為NuSMV中枚舉變量: flow: {feature,feature,…,feature},其中,feature,feature,…,feature對應流s1經過的個特征集合。流的轉移關系用NuSMV中的next()表達式和case語句表示,例如,算法1中從getLocalPlaneAttributeInfo線程的端口和進程MissionLoadP的端口形成的流s3到NuSMV模型的轉換體現(xiàn)了該映射規(guī)則。

    3.3 NuSMV模型的生成算法

    基于上述7條規(guī)則的NuSMV模型生成算法如算法2所示。該算法以AADL模型構件為輸入,以生成的NuSMV模塊為輸出,create表示生成NuSMV元素,VAR表示生成NuSMV變量,ASSIGN表示生成變量的轉移關系,next(var)表示用NuSMV中的next語句描述var的轉移關系。

    算法2描述了AADL構件的NuSMV模型生成方法。該算法的輸入為AADL語言表示的構件A,構件A的生成方法分為以下8步:

    算法2 NuSMV模型生成算法

    1) 首先根據(jù)構件A的構件類型生成對應的NuSMV模塊,按照映射規(guī)則Rule1,如果是system,則創(chuàng)建MODULE_main,否則生成MODULE_component_name,如算法2的第1~5行所示。

    2) 然后根據(jù)構件A包含的子元素類型,生成對應的NuSMV元素。如算法2的第6~50行所示。

    3) 如果構件A包含features,按照映射規(guī)則Rule2生成每個feature對應的feature_MODULE實例,如算法2的第8~12行所示。

    4) 如果構件A包含subcomponents,按照映射規(guī)則Rule3生成每個subcomponent對應的MODULE實例,如算法2的第13~23行所示。

    5) 如果構件A包含connections,按照映射規(guī)則Rule4生成每個connection對應的connection MODULE實例,如算法2的第24~31行所示。

    6) 如果構件A包含modes,按照映射規(guī)則Rule5生成modes變量,如算法2的第32~34行所示。

    7) 如果構件A包含behavior_annex,按照映射規(guī)則Rule6生成behavior MODULE實例,如算法2的第35~42行所示。

    8) 如果構件A包含flows,按照映射規(guī)則Rule7生成每個flow對應的枚舉類型變量,如算法2的第43~49行所示。

    4 AADL模型到NuSMV模型轉換方法的正確性證明

    模型轉換的正確性表現(xiàn)為映射規(guī)則滿足AADL語義保留、確定性以及有限性等性質。本采取圖同構的方法對本文模型轉換方法的正確性進行驗證。

    本文的轉換方法是基于AADL元模型和NuSMV元模型提出的,AADL元模型中的節(jié)點要素到NuSMV元模型中的節(jié)點要素是一一對應的,滿足圖同構的定義。本文通過證明轉換后的NuSMV模型實例與源AADL模型實例語義一致,說明AADL模型到NuSMV轉換方法的正確性。證明思路如圖3所示。

    圖3表示元模型和模型實例之間的映射關系,其中Ins(MMt)指目標語言的模型實例;表示源語言元模型到目標語言源模型的轉換;表示源語言模型實例到目標語言模型實例之間的映射;、′分別表示源語言和目標語言元模型到模型實例之間的映射;表示源語言元模型到目標模型實例之間的映射關系;MMs表示AADL元模型;MMt表示NuSMV的元模型。映射函數(shù)和′為類型保留映射 (Type Prserve Mapping,TPM),TPM由OMG(Object Management Group)定義。

    由3.1節(jié)可知,根據(jù)提出的AADL元模型和NuSMV元模型類圖之間的同構映射,映射函數(shù)是圖同構的。本節(jié)將證明AADL元模型與其模型實例Ins(MM)之間的類型保留映射函數(shù)是圖同構的,同時證明(°)是圖同構的,在此基礎上證明AADL模型實例到NuSMV模型實例的模型轉換函數(shù)是圖同構的。

    定義一個圖同構函數(shù)表示圖從圖到圖的轉換:=(:,:),其中,為圖的節(jié)點集合;為圖節(jié)點到圖節(jié)點集合的映射函數(shù);為圖的節(jié)點集合;為圖邊緣節(jié)點集合到圖邊緣節(jié)點集合的映射函數(shù);為圖的邊緣節(jié)點集合;為圖的邊緣節(jié)點集合。滿足以下約束:

    (1)

    式中:、分別為同時作用于圖的節(jié)點和邊緣節(jié)點的轉換函數(shù)。

    元模型MM為一個UML(Unified Modeling Language)類圖,Ins(MM)為一個UML對象圖。TPM函數(shù)從MM映射為Ins(MM),Ins(MM)中的每一個元素都是MM中類的映射。

    如果元模型MM為UML類圖,模型實例Ins(MM)為UML對象圖。那么在元模型圖及其實例圖之間定義的TPM函數(shù)是圖同構的。

    根據(jù)命題1,在AADL元模型類圖到NuSMV元模型類圖的轉換中,因為AADL元模型元素到其模型實例元素之間,以及NuSMV元模型元素到其模型實例之間的映射都是類型保留映射TPM,所以映射函數(shù)和′是圖同構的。

    如果映射函數(shù)是圖同構的,并且映射函數(shù)是圖同構的,那么和的組合°也是圖同構的。

    根據(jù)命題2,因為函數(shù)、是圖同構的,所以(°)是圖同構的。

    已知在元模型MM和MM′之間存在同構映射,元模型MM和它的實例Ins(MM)之間存在類型保留映射函數(shù),元模型MM′和它的實例Ins(MM′)之間存在類型保留映射函數(shù)′,則Ins(MM)和Ins(MM′)之間的映射函數(shù)是圖同構的。

    如圖3所示,上文已經證明函數(shù)、、′、都是圖同構的,分別用式(2)~式(5)表示

    (MM)=MM’′是圖同構

    (2)

    (MM)=Ins(MM)是圖同構

    (3)

    (MM)=Ins(MM′)是圖同構

    (4)

    (MM)=′((MM))=Ins(MM′)是圖同構的

    (5)

    根據(jù)定義1和式(2),可得

    (6)

    根據(jù)定義1和式(5),可得

    (7)

    假設如圖3所示,=°,將式(7)中的替換成°,可得

    (8)

    根據(jù)式(8),因為是圖同構的,結合定義1的約束,據(jù)此推斷映射函數(shù)也是圖同構的。

    本轉換方法是基于源模型和目標模型的語法結構以及源模型語義角度提出的?;谠茨P秃湍繕四P偷恼Z法結構采用上下文無關文法描述,是精確無二義性的,所以模型轉換為一對一映射,是確定的。同時AADL模型的構成要素是有限的,因此轉換方法是有限的。

    綜上,證明了本文從AADL模型至NuSMV模型轉換方法的正確性。

    5 基于NuSMV模型的驗證方法

    5.1 安全屬性的驗證

    本文驗證的安全屬性(Safety)包括狀態(tài)、模態(tài)的可達性和轉換的確定性。

    5.1.1 可達性驗證

    在狀態(tài)遷移系統(tǒng)中,如果事件或者消息到達指定端口,將會切換為另一個狀態(tài)。狀態(tài)的可達性驗證指在所有可能的狀態(tài)轉換序列中,是否存在目標狀態(tài)不可達的情況。

    1) 模態(tài)可達性驗證

    模態(tài)的可達性指當事件數(shù)據(jù)端口上有事件到達時,一個模態(tài)能夠轉換為另一個模態(tài)的能力。例如,圖4(a)展示了一個由于模態(tài)3沒有傳出轉換導致的非可達性示例,圖4(b)展示了一個滿足模態(tài)可達性的示例。對于圖4,在NuSMV中,表示是否存在從mode1到mode3的模態(tài)轉換序列,模態(tài)可達性的CTL描述為

    AG(modes=mode1→AF(modes=mode3))

    (9)

    2) 行為附件狀態(tài)可達性驗證

    行為附件狀態(tài)的可達性指衛(wèi)式(Guard)滿足時,從一個行為狀態(tài)切換到另一個行為狀態(tài)的能力,衛(wèi)式是指狀態(tài)轉換時滿足的約束條件。例如,圖5(a)表示由于s1和s2沒有傳出轉換,所以從s2到s1,或從s1到s2都是不可達的;圖5(b) 表示了一個狀態(tài)可達的案例。在NuSMV中,表示是否存在從s1到s2的行為狀態(tài)轉換序列,行為附件狀態(tài)的可達性CTL描述為

    AG((states=s1) →AF(states=s2))

    (10)

    圖4 模態(tài)可達性示例Fig.4 Example of mode reachability

    圖5 行為狀態(tài)可達性Fig.5 Example of state reachability

    5.1.2 確定性驗證

    狀態(tài)轉換分為確定性和非確定性。在一個狀態(tài)上,對于同一個轉換條件,有且只有一條轉換,則稱該轉換是確定性的,否則為非確定性的。AADL模型中的模態(tài)和行為狀態(tài)轉換必須是確定性的。例如,圖6(a)所示為當port1上的事件到達時,模態(tài)會從mode1向mode2轉換,或向mode3轉換,這屬于非確定性的模態(tài)轉換;圖6(b) 所示為確定性的模態(tài)轉換案例,對每一個源模態(tài),每一個轉換條件只存在唯一的傳出轉換。NuSMV表示到mode2模態(tài)的轉換是否是確定性的,對應的CTL規(guī)范描述為

    AF modes = mode2

    (11)

    圖6 模態(tài)轉換的確定性Fig.6 Example of deterministic mode transition

    5.2 活性屬性的驗證

    活性屬性指“計劃的事情最終一定會發(fā)生”。活性屬性驗證包括進度屬性的驗證。進度屬性指“如果滿足某些條件,某些事情最終一定會發(fā)生”。AADL模態(tài)切換、行為附件中行為狀態(tài)的切換皆定義了進度屬性。NuSMV中,如果模態(tài)切換的條件(Event)滿足,模態(tài)將會按照計劃切換為mode2,模態(tài)進度屬性的CTL規(guī)范描述為:AG(event →AF(modes=mode2));如果行為狀態(tài)轉換的條件滿足,行為狀態(tài)將會按照計劃變成S0狀態(tài),行為附件中行為狀態(tài)的進度屬性對應的CTL規(guī)范描述為

    AG(event → AF(states=S0))

    (12)

    5.3 模態(tài)配置的合法性驗證

    AADL模型中,構件對其所包含的子構件、連接等元素與模態(tài)的關聯(lián)性進行配置,表示不同操作狀態(tài)下的構件行為。本文對模態(tài)配置的合法性驗證包括連接元素模態(tài)配置的合法性驗證、子構件模態(tài)配置的合法性驗證、流元素模態(tài)配置的合法性驗證及系統(tǒng)構件下線程行為嵌套配置的合法性驗證4部分。

    1) 連接元素模態(tài)配置的合法性驗證

    AADL模型中連接表示不同構件之間的數(shù)據(jù)交互,連接元素模態(tài)配置的合法性指構件間的數(shù)據(jù)交互是否符合模態(tài)配置的要求。NuSMV中,conn1只在模態(tài)mode1下有效的性質對應的CTL規(guī)范描述為

    A[!conn1.is Working U modes=mode1]

    (13)

    2) 子構件模態(tài)配置的合法性驗證

    AADL模型中,不同的模態(tài)指定了構件不同的操作狀態(tài)。子構件模態(tài)配置的合法性指子構件的有效性是否符合構件模態(tài)配置的要求。映射規(guī)則Rule1中提到,進程模塊的isActive屬性標識進程模塊是否在系統(tǒng)模塊的模態(tài)配置下有效;線程模塊的isBehavior屬性標識線程模塊是否在進程模塊的模態(tài)配置下有效。NuSMV中,表示進程模塊p在系統(tǒng)模態(tài)mode1下是否有效的CTL規(guī)范描述為

    AF(modes=mode1 & p.is Active)

    (14)

    3) 流元素模態(tài)配置的合法性驗證

    AADL模型中,因為流元素的合法性與連接的合法性及子構件的合法性有關。所以流的可達性與模態(tài)配置具有一定的關聯(lián)關系。

    NuSMV中,表示在模態(tài)mode1下,流flow是否可以達到指定的特征接口,流元素模態(tài)配置的合法性屬性對應的CTL規(guī)范描述為

    AG(modes=mode1)→AF(flow=feature))

    (15)

    4) 系統(tǒng)構件下線程行為模態(tài)嵌套的合法性驗證

    AADL模型中,系統(tǒng)構件的模態(tài)配置影響進程構件的有效性,進程構件的模態(tài)配置影響線程子構件的行為執(zhí)行。所以系統(tǒng)構件的模態(tài)配置,會間接對具體線程的行為執(zhí)行產生影響。

    系統(tǒng)構件下線程行為配置的合法性驗證就是判斷線程行為的有效性是否符合系統(tǒng)定義的模態(tài)配置。NuSMV中,表示在系統(tǒng)模態(tài)mode2下,進程構件p中的線程構件t是否能夠正常執(zhí)行,該性質對應的CTL規(guī)范描述為

    AF(modes=mode2 & p.t.is Behavior)

    (16)

    6 實驗驗證

    以包含人機交互子系統(tǒng)、備份子系統(tǒng)和自動飛行子系統(tǒng)的飛行控制系統(tǒng)為例,詳細闡釋了基于NuSMV的AADL模型形式化驗證方法。

    6.1 實驗案例

    人機交互子系統(tǒng)負責處理飛行員對飛機的操作指令,并且負責顯示飛機的各項飛行參數(shù)。該子系統(tǒng)包含了顯示控制進程和飛行員輸入進程。顯示進程將飛機的飛行參數(shù)展示給飛行員,并且根據(jù)飛行員的操作控制駕駛桿、油門桿和周邊鍵等設備。飛行員輸入進程包含3個分別處于不同計算機上的飛行員輸入線程,當1個輸入線程發(fā)生異常時,會由其他飛行員輸入線程完成對飛行員輸入信息的處理。

    備份子系統(tǒng)的主要功能為備份重要的數(shù)據(jù)信息,當飛行控制系統(tǒng)發(fā)生異常狀況時,能夠根據(jù)備份信息恢復正常,備份子系統(tǒng)運行在PowerPC_G4處理器上。

    自動飛行子系統(tǒng)主要功能為讀取GPS(Global Positioning System)數(shù)據(jù),發(fā)送控制信號至控制平臺實現(xiàn)飛機的自動飛行,該子系統(tǒng)包括GPS讀取線程以及自動導航線程。GPS讀取線程僅在初始狀態(tài)從GPS讀取飛機位置信息,當開啟自動駕駛后,自動導航線程開始運行,飛機進入自動駕駛狀態(tài)。

    6.2 實驗案例——飛行控制系統(tǒng)的AADL模型

    使用OSATE工具為飛行控制系統(tǒng)建模。該AADL模型包括人機交互子系統(tǒng)S_HCI、自動飛行子系統(tǒng)S_NAP和備份子系統(tǒng)S_BUP。

    S_HCI包含1個飛行員輸入進程構件P_Pinput和1個顯示控制進程構件P_DIS,表示駕駛桿、油門桿和周邊鍵的設備構件以及表示線程運行平臺的處理器構件。P_Pinput包含3個綁定到不同處理器的飛行員輸入線程T_Pilot_Input1、T_Pilot_Input2、T_Pilot_Input3。同時P_Pinput包含3個輸入線程的模態(tài)配置,表示不同情況下不同線程的執(zhí)行情況。飛行員輸入線程為后臺線程,當飛行員輸入命令的時候會啟動。P_DIS包括2個線程構件顯示線程T_Screen_Disp和設備控制線程T_Control_Dev。顯示線程每50 ms會刷新界面顯示,設備控制線程根據(jù)飛行員輸入信息控制駕駛桿、油門桿和周邊鍵3個設備。

    S_NAP中有2個模態(tài):加載(load)和執(zhí)行(run)。當自動飛行子系統(tǒng)接收到自動駕駛打開的事件,模態(tài)會由load變?yōu)閞un。導航控制進程P_Nav_Con只在run模態(tài)下正常執(zhí)行。P_Nav_Con包含GPS讀取線程T_GPS_Reader和自動導航計算線程T_AP_Compute,該進程構件有3種工作模態(tài),即:GPS打開及自動導航關閉模態(tài)GPS_UP_AP_DOWN、GPS打開及自動導航打開模態(tài)GPS_UP_AP_UP、GPS關閉模態(tài)GPS_DOWN。如果GPS出現(xiàn)故障時,飛行控制系統(tǒng)不能自動飛行。

    S_BUP包含1個備份進程構件P_BUP和PowerPC_G4處理器構件,P_BUP包含1個數(shù)據(jù)庫訪問線程構件T_DB_Operation,主要負責訪問數(shù)據(jù)庫中的備份信息,該線程構件與PowerPC_G4處理器構件的關系通過S_BUP子系統(tǒng)構件的Actual_Processor_Binding屬性表示。

    當導航控制進程處在GPS_UP_AP_DOWN模態(tài)時,如果飛行員將飛機駕駛狀態(tài)調整為自動駕駛,則模態(tài)會變成GPS_UP_AP_UP模態(tài),如果GPS發(fā)生故障,模態(tài)將會變成GPS_DOWN模態(tài)。T_GPS_Reader線程在GPS_UP_AP_DOWN和GPS_UP_AP_UP模態(tài)下都可以正常工作。該線程每隔20 ms從GPS獲取一次數(shù)據(jù)。T_AP_Compute線程僅在GPS_UP_AP_UP模態(tài)下正常工作,該線程每隔50 ms會輸出一次飛機的俯仰角、偏航角、滾動角信息給制動器,以實現(xiàn)飛機自動導航。

    6.3 生成的實驗案例——飛行控制系統(tǒng)的NuSMV模型

    基于AADL模型到NuSMV模型的映射規(guī)則和轉換算法,構建飛行控制系統(tǒng)的NuSMV模型。NuSMV模型包括:1個main模塊,S_HCI、S_NAP和S_BUP 3個子系統(tǒng)模塊,P_Pinput、P_DIS、P_BUP和P_Nav_Con 4個進程模塊,T_Pilot_Input1、T_Pilot_In put 2、T_Polot_Input 3、T_Screen_Disp、T_Control_Dev、T_DB_Operation、T_GPS_Reader和T_AP_Compute 8個線程模塊以及表示線程模塊行為的行為附件模塊;3個數(shù)據(jù)模塊。例如,生成的P_Nav_Con進程模塊(導航控制進程)如算法3所示,其中modes變量的轉移關系如算法4所示,T_GPS_Reader線程模塊及其行為附件模塊如算法5所示。

    算法3 導航控制進程模塊

    算法4 modes變量的轉換關系

    算法5 線程模塊及其行為附件模塊Algorithm 5 Thread module and behavior_annex module

    6.4 實驗案例——飛行控制系統(tǒng)的形式化驗證

    基于飛行控制系統(tǒng)NuSMV形式化模型,對其安全屬性、活性屬性以及模態(tài)配置的合法性進行驗證,如果相應屬性的驗證結果為TRUE,則表示驗證屬性符合要求;否則NuSMV會給出一條反例路徑,說明驗證失敗的原因,模型驗證人員可以根據(jù)反例路徑去完善建模方案。

    6.4.1 安全屬性的驗證

    安全屬性驗證包括可達性及確定性的驗證。

    1)可達性驗證

    ①Nav_Control_Process模塊modes的可達性驗證

    如果當前模態(tài)為GPS_UP_AP_DOWN,驗證GPS_UP_AP_UP是否可達,該屬性對應的CTL規(guī)范為

    AG(modes=GPS_UP_AP_DOWN→

    AF(modes=GPS_UP_AP_UP))

    (17)

    驗證結果為TRUE表示Nav_Control_Process進程的GPS_UP_AP_UP模態(tài)滿足從GPS_UP_AP_DOWN模態(tài)開始的可達性,否則模型存在故障。

    ② T_GPS_Reader行為狀態(tài)的可達性驗證

    T_GPS_Reader的行為附件的reader1狀態(tài)表示該線程調度完成,驗證reader1行為狀態(tài)是否可達。該屬性對應的CTL規(guī)范為

    AG(states=reader0→EF(states=reader1))

    (18)

    驗證結果為TRUE表示T_GPS_Reader可以被正常調度,否則存在故障。

    2)確定性驗證。

    對Nav_Control_Process的GPS_DOWN模態(tài)進行確定性方面的驗證,模態(tài)的確定性保證了構件不同的操作行為都可以正常執(zhí)行。該屬性對應的CTL規(guī)范為

    AF modes=GPS_DOWN

    (19)

    驗證結果為FALSE,對NuSMV工具給出的反例路徑進行查看,發(fā)現(xiàn)如果GPS_error事件一直未發(fā)生,進程模態(tài)就不會變成GPS_DOWN。在實際情況中,GPS錯誤事件有一定概率發(fā)生,這是由于未添加公平性約束導致的驗證結果與預期不符。對GPS_error變量添加公平性約束并重新驗證,模型滿足該條屬性。

    6.4.2 活性屬性的驗證

    1) Nav_Control_Process的GPS_UP_AP_UP模態(tài)的活性驗證

    GPS_UP_AP_UP表示GPS打開及自動導航打開模態(tài),當人機交互子系統(tǒng)設置飛機為自動駕駛狀態(tài)時,導航控制進程會接收到自動導航指令,工作模態(tài)也會變成GPS_UP_AP_UP。該屬性對應的CTL規(guī)范為

    AG(AP_Toggle_event→AF(modes=

    GPS_UP_AP_UP))

    (20)

    驗證結果為TRUE表示一旦飛行員設置飛機飛行狀態(tài)為自動駕駛,Nav_Control_Process進程會在GPS打開及自動導航打開(GPS_UP_AP_UP)模態(tài)下執(zhí)行。

    2) T_GPS_Reader行為狀態(tài)的活性屬性驗證

    當T_GPS_Reader接收到改變駕駛狀態(tài)的消息時,T_GPS_Reader會自動獲取飛機位置信息。該屬性對應的CTL規(guī)范為

    AG(AP_Position_Input_event→AF(behavior_

    specification.states=reader1))

    (21)

    驗證結果為TRUE表示T_GPS_Reader線程只要接收到改變駕駛狀態(tài)的消息時,總會成功執(zhí)行其行為;否則模型存在故障。

    6.4.3 模態(tài)配置的合法性驗證

    1) 連接元素模態(tài)配置的合法性驗證

    當Nav_Control_Process以GPS_UP_AP_UP模態(tài)工作時,與自動導航計算線程T_AP_Compute線程有關的連接應該是有效的。該屬性對應的CTL規(guī)范為

    A[!conn1.is Working U modes=

    GPS_UP_AP_UP]

    (22)

    驗證結果為TRUE表示在模態(tài)為GPS_UP_AP_UP時,連接conn1總是有效的,否則存在故障。

    2) 子構件模態(tài)配置的合法性驗證

    T_AP_Compute僅在GPS_UP_AP_UP模態(tài)下才正常執(zhí)行。該屬性對應的CTL規(guī)范為

    AF(modes=GPS_UP_AP_UP &

    T_AP_Compute.is Behavior)

    (23)

    驗證結果為TRUE表示T_AP_Compute符合Nav_Control_Process的模態(tài)配置定義,僅在GPS_UP_AP_UP模態(tài)下執(zhí)行,否則存在故障。

    3) 流元素模態(tài)配置的合法性驗證

    AADL模型中定義的數(shù)據(jù)流data,只有在模態(tài)GPS_UP_AP_UP下,才可以到達滾動角輸出接口(Delta_Roll_Output)。該屬性對應的CTL規(guī)范為

    AG(modes=GPS_UP_AP_UP→AF(data=

    Delta_Roll_Output))

    (24)

    驗證結果為TRUE表示在GPS_UP_AP_UP模態(tài)下,流data總能達到滾動角輸出接口,即流的有效性符合Nav_Control_Process的模態(tài)配置定義,否則存在故障。

    4) 系統(tǒng)構件下線程行為配置的合法性驗證Nav_Control_Process進程僅在自動飛行子系統(tǒng)模態(tài)為run時,才會正常執(zhí)行。而Nav_Control_Process內的T_AP_Compute線程僅在進程模態(tài)為GPS_UP_AP_UP時,才會執(zhí)行。驗證系統(tǒng)模態(tài)為run模態(tài)時,T_AP_Compute線程是否會正常執(zhí)行。該屬性對應的CTL規(guī)范為

    AF (modes=run & Nav_Control_Process.

    T_AP_Compute.is Behavior)

    (25)

    驗證結果為TRUE表示T_AP_Compute的行為符合系統(tǒng)模態(tài)的配置定義,否則存在故障。

    6.5 驗證結果分析

    通過在AADL模型中插入10種故障類型,形成不同的AADL故障設計模型,并對其進行驗證,均可以發(fā)現(xiàn)相應的故障,證明了本文方法的有效性。通過對飛行控制系統(tǒng)的驗證結果進行分析,實驗結果統(tǒng)計信息(包括故障說明、驗證故障數(shù)目、驗證故障總數(shù)、驗證消耗時間和空間)如表2 所示。

    表3展示了本文提出的基于NuSMV的AADL模型形式化驗證方法與其他方法的對比結果,通過對比,本文方法主要具有以下3個方面的優(yōu)勢:

    1) 考慮的AADL子集更豐富,包括構件、特征、連接、模態(tài)、數(shù)據(jù)流及行為附件等建模元素。

    2) 采用圖同構的方法保留AADL模型語義,以保證AADL模型到NuSMV模型轉換的正確性、有效性和有限性。

    3) 對AADL模型中的安全性、活性、模態(tài)配置的正確性進行驗證,其中模態(tài)配置驗證包括連接子元素、子構件及流元素的模態(tài)配置,以及系統(tǒng)層次化建模導致的模態(tài)嵌套正確性的驗證。

    7 結 論

    本文覆蓋了全部AADL軟構件、系統(tǒng)和構件行為、模態(tài)配置和模態(tài)嵌套相關的建模要素,提出了一種基于NuSMV的AADL模型形式化驗證方法,以驗證AADL模型中安全性、活性和任務屬性配置模態(tài)的正確性。由于NuSMV自身的缺陷,部分屬性無法驗證,比如模型精化屬性、可調度性。所以本文與團隊之前發(fā)表的文獻[7]分別使用2種形式化方法對AADL模型進行驗證,兩種方法的側重點不同,具有互補性。

    表2 實驗結果統(tǒng)計信息Table 2 Statistics of experimental results

    表3 相關工作比較Table 3 Comparison of related works

    續(xù)表3

    猜你喜歡
    線程進程實例
    債券市場對外開放的進程與展望
    中國外匯(2019年20期)2019-11-25 09:54:58
    淺談linux多線程協(xié)作
    完形填空Ⅱ
    完形填空Ⅰ
    社會進程中的新聞學探尋
    民主與科學(2014年3期)2014-02-28 11:23:03
    我國高等教育改革進程與反思
    Linux僵死進程的產生與避免
    Linux線程實現(xiàn)技術研究
    么移動中間件線程池并發(fā)機制優(yōu)化改進
    JAVA多線程同步解決生產者—消費者問題
    亚洲一区二区三区不卡视频| 国产一区二区三区视频了| www.自偷自拍.com| 久久婷婷人人爽人人干人人爱| 亚洲国产欧美人成| 在线观看免费日韩欧美大片| 欧美中文日本在线观看视频| 日韩欧美在线乱码| 小说图片视频综合网站| 人人妻人人澡欧美一区二区| 精品乱码久久久久久99久播| av超薄肉色丝袜交足视频| 国产99白浆流出| 亚洲美女黄片视频| 国产亚洲欧美在线一区二区| 久久午夜亚洲精品久久| 91大片在线观看| 老司机在亚洲福利影院| 一级a爱片免费观看的视频| 国产三级黄色录像| 久久午夜亚洲精品久久| 欧美久久黑人一区二区| 欧美精品啪啪一区二区三区| 亚洲自拍偷在线| 中文字幕熟女人妻在线| 亚洲成人久久爱视频| 怎么达到女性高潮| 一区二区三区激情视频| 亚洲激情在线av| 久久亚洲真实| 校园春色视频在线观看| 日韩国内少妇激情av| 精品人妻1区二区| 国产精品日韩av在线免费观看| 成年人黄色毛片网站| 最新美女视频免费是黄的| 国产精品1区2区在线观看.| 日韩 欧美 亚洲 中文字幕| 精品国产乱码久久久久久男人| 中文字幕精品亚洲无线码一区| 99精品在免费线老司机午夜| 人妻夜夜爽99麻豆av| 日韩欧美三级三区| 十八禁人妻一区二区| 久久久久精品国产欧美久久久| 中文字幕av在线有码专区| 熟妇人妻久久中文字幕3abv| 老熟妇仑乱视频hdxx| 日本五十路高清| 亚洲人成77777在线视频| 国产麻豆成人av免费视频| 国产精品野战在线观看| 午夜福利高清视频| 变态另类丝袜制服| 欧美色视频一区免费| 亚洲欧美日韩高清在线视频| 亚洲精品中文字幕在线视频| 岛国视频午夜一区免费看| 麻豆av在线久日| 亚洲第一电影网av| 亚洲专区国产一区二区| 在线永久观看黄色视频| 亚洲国产欧美一区二区综合| 亚洲精品国产一区二区精华液| 又黄又爽又免费观看的视频| 中文字幕人成人乱码亚洲影| 岛国在线免费视频观看| 人妻久久中文字幕网| 成人高潮视频无遮挡免费网站| 美女大奶头视频| 一夜夜www| 久久草成人影院| 国产精品乱码一区二三区的特点| 成人三级黄色视频| 少妇裸体淫交视频免费看高清 | 日韩精品中文字幕看吧| 午夜福利欧美成人| 人成视频在线观看免费观看| 亚洲avbb在线观看| 亚洲av五月六月丁香网| 日本 av在线| 亚洲精华国产精华精| 色尼玛亚洲综合影院| 黄色成人免费大全| 国产私拍福利视频在线观看| 久久性视频一级片| 黄色a级毛片大全视频| 麻豆久久精品国产亚洲av| 国产欧美日韩精品亚洲av| 欧美日韩福利视频一区二区| 一区二区三区国产精品乱码| 日本五十路高清| 一夜夜www| 精品久久久久久成人av| 亚洲欧美精品综合一区二区三区| 久久精品国产清高在天天线| 成人手机av| 夜夜躁狠狠躁天天躁| 午夜视频精品福利| 色综合站精品国产| 这个男人来自地球电影免费观看| 国产日本99.免费观看| 成人18禁在线播放| 国产成人欧美在线观看| 免费在线观看亚洲国产| 中文在线观看免费www的网站 | 国产一区二区在线观看日韩 | 欧美国产日韩亚洲一区| 黄色毛片三级朝国网站| 亚洲国产精品合色在线| 久久婷婷成人综合色麻豆| 日韩欧美一区二区三区在线观看| 国产精品爽爽va在线观看网站| 51午夜福利影视在线观看| 在线观看免费日韩欧美大片| 女警被强在线播放| 成人三级做爰电影| 久久 成人 亚洲| 久久国产精品影院| 天天躁狠狠躁夜夜躁狠狠躁| 中文字幕人妻丝袜一区二区| cao死你这个sao货| 国产亚洲欧美98| 中文字幕久久专区| 国产精品亚洲一级av第二区| 欧美在线黄色| 亚洲人成77777在线视频| 久久久国产成人免费| 日韩欧美国产在线观看| 人妻夜夜爽99麻豆av| 久久久久久大精品| 久久精品国产99精品国产亚洲性色| 亚洲一区中文字幕在线| 嫩草影视91久久| 少妇人妻一区二区三区视频| 中文字幕人成人乱码亚洲影| 香蕉久久夜色| 夜夜看夜夜爽夜夜摸| 亚洲国产精品999在线| 欧美日韩中文字幕国产精品一区二区三区| av超薄肉色丝袜交足视频| 91麻豆av在线| 国产精品 欧美亚洲| 欧美日韩国产亚洲二区| 精品人妻1区二区| 亚洲av日韩精品久久久久久密| 久久人妻福利社区极品人妻图片| 一本久久中文字幕| 女人被狂操c到高潮| 亚洲精品av麻豆狂野| 久久久久久免费高清国产稀缺| 美女黄网站色视频| 欧美日韩一级在线毛片| 超碰成人久久| 一进一出好大好爽视频| 久久久国产成人免费| 好看av亚洲va欧美ⅴa在| av在线播放免费不卡| 男人的好看免费观看在线视频 | 亚洲av日韩精品久久久久久密| 可以免费在线观看a视频的电影网站| 国产黄片美女视频| 波多野结衣高清作品| 99热6这里只有精品| 亚洲午夜精品一区,二区,三区| 美女高潮喷水抽搐中文字幕| 国内精品久久久久久久电影| 激情在线观看视频在线高清| 美女高潮喷水抽搐中文字幕| 99久久精品国产亚洲精品| 亚洲一区中文字幕在线| 亚洲国产欧洲综合997久久,| 18禁黄网站禁片午夜丰满| 757午夜福利合集在线观看| 国产精品,欧美在线| av福利片在线| 免费在线观看视频国产中文字幕亚洲| 色综合亚洲欧美另类图片| 操出白浆在线播放| 婷婷亚洲欧美| 亚洲精品美女久久久久99蜜臀| 精品无人区乱码1区二区| 精品福利观看| 天堂√8在线中文| 欧美3d第一页| 欧美三级亚洲精品| 黄色视频,在线免费观看| 成人18禁在线播放| 久久精品人妻少妇| 国产精品 国内视频| 啦啦啦观看免费观看视频高清| 色在线成人网| 这个男人来自地球电影免费观看| 亚洲中文日韩欧美视频| 久久99热这里只有精品18| 久99久视频精品免费| 成人一区二区视频在线观看| 国产一区二区三区视频了| 婷婷六月久久综合丁香| 天天添夜夜摸| 禁无遮挡网站| 久久人妻av系列| 国产亚洲精品久久久久久毛片| 久久这里只有精品中国| 免费人成视频x8x8入口观看| 老司机午夜福利在线观看视频| 亚洲自偷自拍图片 自拍| 无遮挡黄片免费观看| 久久中文字幕一级| 国产单亲对白刺激| 一本大道久久a久久精品| 久久欧美精品欧美久久欧美| 听说在线观看完整版免费高清| 女人被狂操c到高潮| 日本黄色视频三级网站网址| 国产亚洲精品久久久久5区| 国产aⅴ精品一区二区三区波| av中文乱码字幕在线| 免费看十八禁软件| 中文资源天堂在线| 1024香蕉在线观看| 又爽又黄无遮挡网站| 国产午夜福利久久久久久| 一个人免费在线观看电影 | 亚洲人成网站在线播放欧美日韩| 精品久久久久久久毛片微露脸| 高清在线国产一区| 日本五十路高清| 黄片大片在线免费观看| 国产精品亚洲美女久久久| 岛国视频午夜一区免费看| 精品久久蜜臀av无| 免费在线观看影片大全网站| 69av精品久久久久久| 日日夜夜操网爽| avwww免费| 黄色片一级片一级黄色片| 婷婷精品国产亚洲av| a级毛片a级免费在线| 天堂影院成人在线观看| 无遮挡黄片免费观看| 亚洲色图 男人天堂 中文字幕| 亚洲欧美日韩东京热| 十八禁网站免费在线| 中出人妻视频一区二区| 一区二区三区高清视频在线| 99久久无色码亚洲精品果冻| 日日摸夜夜添夜夜添小说| 亚洲美女视频黄频| 97超级碰碰碰精品色视频在线观看| 国产亚洲av高清不卡| 国内毛片毛片毛片毛片毛片| 精品一区二区三区av网在线观看| 巨乳人妻的诱惑在线观看| 别揉我奶头~嗯~啊~动态视频| 激情在线观看视频在线高清| 最近视频中文字幕2019在线8| 伦理电影免费视频| 日韩欧美精品v在线| 久9热在线精品视频| 成年版毛片免费区| 久久中文字幕人妻熟女| 啦啦啦观看免费观看视频高清| 国产主播在线观看一区二区| av片东京热男人的天堂| 亚洲电影在线观看av| 大型av网站在线播放| 99久久99久久久精品蜜桃| 日本精品一区二区三区蜜桃| 欧美日韩亚洲国产一区二区在线观看| 男人舔女人的私密视频| 男人的好看免费观看在线视频 | 男插女下体视频免费在线播放| 在线十欧美十亚洲十日本专区| 久久久久久国产a免费观看| 国产激情久久老熟女| 人人妻,人人澡人人爽秒播| 一本久久中文字幕| 曰老女人黄片| 极品教师在线免费播放| 一级毛片精品| 国产高清videossex| 波多野结衣高清无吗| 91国产中文字幕| 婷婷亚洲欧美| 日韩欧美免费精品| 男女那种视频在线观看| 久久精品aⅴ一区二区三区四区| 久久久精品国产亚洲av高清涩受| 又紧又爽又黄一区二区| 亚洲一码二码三码区别大吗| 国产亚洲精品一区二区www| 九色成人免费人妻av| 一本精品99久久精品77| 色噜噜av男人的天堂激情| 操出白浆在线播放| 国产一级毛片七仙女欲春2| 亚洲黑人精品在线| 国产精品亚洲美女久久久| 久久精品综合一区二区三区| 人妻丰满熟妇av一区二区三区| 国产高清激情床上av| 欧美3d第一页| 99国产极品粉嫩在线观看| 好男人在线观看高清免费视频| 又紧又爽又黄一区二区| 久久久久久久精品吃奶| 熟妇人妻久久中文字幕3abv| 舔av片在线| 国产精品野战在线观看| 亚洲av成人av| 国产又黄又爽又无遮挡在线| 一区福利在线观看| 狂野欧美激情性xxxx| 亚洲精品在线观看二区| 18禁黄网站禁片午夜丰满| 亚洲精品中文字幕在线视频| 18禁裸乳无遮挡免费网站照片| 手机成人av网站| 国产亚洲精品久久久久5区| 亚洲av成人一区二区三| 亚洲av成人av| 夜夜躁狠狠躁天天躁| 亚洲激情在线av| www.精华液| 丁香欧美五月| 亚洲免费av在线视频| 又粗又爽又猛毛片免费看| 久9热在线精品视频| 精品国产亚洲在线| 十八禁人妻一区二区| 国产黄片美女视频| 免费人成视频x8x8入口观看| 欧美日韩瑟瑟在线播放| 日本免费a在线| 91九色精品人成在线观看| 久久久国产精品麻豆| 精品国内亚洲2022精品成人| 丰满人妻一区二区三区视频av | 岛国在线免费视频观看| 超碰成人久久| 黄频高清免费视频| 91九色精品人成在线观看| 91成年电影在线观看| 国产1区2区3区精品| 国产精品一区二区三区四区久久| 久久午夜综合久久蜜桃| 国产私拍福利视频在线观看| 日本在线视频免费播放| 国产精品av视频在线免费观看| 97超级碰碰碰精品色视频在线观看| 精品电影一区二区在线| 香蕉国产在线看| 老司机深夜福利视频在线观看| 男人舔女人下体高潮全视频| 午夜福利视频1000在线观看| 韩国av一区二区三区四区| 久久这里只有精品中国| 美女 人体艺术 gogo| 亚洲一区中文字幕在线| 午夜福利免费观看在线| www国产在线视频色| 日韩中文字幕欧美一区二区| 在线观看美女被高潮喷水网站 | 国产亚洲欧美98| 成人永久免费在线观看视频| 91麻豆精品激情在线观看国产| 国产精品美女特级片免费视频播放器 | 在线免费观看的www视频| 黄色片一级片一级黄色片| 欧美 亚洲 国产 日韩一| 亚洲国产精品999在线| 成人午夜高清在线视频| 国产在线精品亚洲第一网站| 99国产极品粉嫩在线观看| 国产午夜精品久久久久久| 久久久国产精品麻豆| 亚洲人与动物交配视频| 亚洲 欧美 日韩 在线 免费| av超薄肉色丝袜交足视频| 又黄又粗又硬又大视频| 天堂√8在线中文| 欧美另类亚洲清纯唯美| 亚洲国产精品999在线| av福利片在线| 国产黄片美女视频| 午夜福利免费观看在线| 高清在线国产一区| 无遮挡黄片免费观看| 国产麻豆成人av免费视频| 亚洲精品中文字幕在线视频| 亚洲精品久久国产高清桃花| 激情在线观看视频在线高清| 俄罗斯特黄特色一大片| 国产av麻豆久久久久久久| 国产在线观看jvid| 一本一本综合久久| 亚洲欧美精品综合一区二区三区| 亚洲一码二码三码区别大吗| 欧美乱码精品一区二区三区| 久久久水蜜桃国产精品网| svipshipincom国产片| 午夜福利欧美成人| 久久久精品国产亚洲av高清涩受| 三级国产精品欧美在线观看 | 99国产综合亚洲精品| 人妻丰满熟妇av一区二区三区| 亚洲精品久久成人aⅴ小说| 欧美色欧美亚洲另类二区| 一区二区三区高清视频在线| 两个人视频免费观看高清| 国产亚洲精品av在线| 天堂动漫精品| 级片在线观看| avwww免费| 欧美黄色淫秽网站| 亚洲成人免费电影在线观看| 亚洲av第一区精品v没综合| 中文字幕久久专区| 人人妻人人澡欧美一区二区| 久久性视频一级片| 老熟妇乱子伦视频在线观看| 中文字幕熟女人妻在线| 50天的宝宝边吃奶边哭怎么回事| 国内揄拍国产精品人妻在线| 国产亚洲欧美98| 少妇粗大呻吟视频| 男人的好看免费观看在线视频 | 日本a在线网址| 波多野结衣巨乳人妻| 亚洲精品美女久久久久99蜜臀| 丰满人妻熟妇乱又伦精品不卡| 亚洲自拍偷在线| 国产麻豆成人av免费视频| 亚洲中文字幕一区二区三区有码在线看 | 精品国产美女av久久久久小说| 狂野欧美激情性xxxx| 神马国产精品三级电影在线观看 | 操出白浆在线播放| 亚洲电影在线观看av| 精品熟女少妇八av免费久了| 亚洲精品在线观看二区| 校园春色视频在线观看| 亚洲男人天堂网一区| 99精品在免费线老司机午夜| 精品国产乱码久久久久久男人| 成人国产综合亚洲| 高清毛片免费观看视频网站| 好男人电影高清在线观看| e午夜精品久久久久久久| 国产真人三级小视频在线观看| 高清在线国产一区| 亚洲精品粉嫩美女一区| 久久精品亚洲精品国产色婷小说| 精品久久久久久久末码| 成人av一区二区三区在线看| 欧美黄色淫秽网站| 他把我摸到了高潮在线观看| 国产精品电影一区二区三区| 日本免费a在线| 黄色成人免费大全| 别揉我奶头~嗯~啊~动态视频| 国产av在哪里看| 熟女少妇亚洲综合色aaa.| 宅男免费午夜| 成人精品一区二区免费| 日本a在线网址| 黑人巨大精品欧美一区二区mp4| 国产熟女午夜一区二区三区| 天天躁狠狠躁夜夜躁狠狠躁| 天堂影院成人在线观看| 国产精品日韩av在线免费观看| 一本大道久久a久久精品| 久久天躁狠狠躁夜夜2o2o| 身体一侧抽搐| 欧美3d第一页| 18禁黄网站禁片免费观看直播| 久久精品国产99精品国产亚洲性色| 最好的美女福利视频网| 亚洲精品中文字幕一二三四区| 色播亚洲综合网| 中文字幕av在线有码专区| 久久久久久久午夜电影| 黄色毛片三级朝国网站| 露出奶头的视频| 亚洲成av人片在线播放无| 欧美日韩乱码在线| 国产精品乱码一区二三区的特点| 我要搜黄色片| 亚洲自偷自拍图片 自拍| 舔av片在线| 99国产精品99久久久久| 久久久久久国产a免费观看| 国产亚洲精品综合一区在线观看 | 特大巨黑吊av在线直播| 国产主播在线观看一区二区| 日韩欧美国产在线观看| 欧美黄色片欧美黄色片| 国产成人av激情在线播放| 免费高清视频大片| 可以在线观看毛片的网站| 久久久久久大精品| 久久久久免费精品人妻一区二区| 国产精品自产拍在线观看55亚洲| 特级一级黄色大片| 国产精品久久久久久人妻精品电影| 亚洲va日本ⅴa欧美va伊人久久| 大型av网站在线播放| 亚洲最大成人中文| 亚洲一码二码三码区别大吗| 亚洲色图av天堂| 亚洲五月天丁香| 欧美精品亚洲一区二区| 中亚洲国语对白在线视频| 黑人巨大精品欧美一区二区mp4| 国产精华一区二区三区| 动漫黄色视频在线观看| 久久久国产成人免费| 色哟哟哟哟哟哟| 亚洲一卡2卡3卡4卡5卡精品中文| 久久久久久免费高清国产稀缺| 这个男人来自地球电影免费观看| 老司机在亚洲福利影院| 黄频高清免费视频| 亚洲自偷自拍图片 自拍| 亚洲九九香蕉| 一本大道久久a久久精品| 亚洲性夜色夜夜综合| 欧美日本视频| 国产精品av久久久久免费| 久久久久免费精品人妻一区二区| 亚洲性夜色夜夜综合| 无限看片的www在线观看| 51午夜福利影视在线观看| 国产精品乱码一区二三区的特点| 制服丝袜大香蕉在线| 欧美精品啪啪一区二区三区| 91av网站免费观看| 亚洲国产日韩欧美精品在线观看 | 久久久久国产精品人妻aⅴ院| 岛国在线免费视频观看| 国产激情久久老熟女| 国产黄片美女视频| 欧美成人性av电影在线观看| 国产精品乱码一区二三区的特点| 午夜亚洲福利在线播放| 国产激情欧美一区二区| 亚洲av成人av| 久久热在线av| 88av欧美| 亚洲精品av麻豆狂野| 午夜福利免费观看在线| 一本综合久久免费| 岛国在线免费视频观看| 国产精品免费视频内射| 男人的好看免费观看在线视频 | 精品国产乱码久久久久久男人| 国产精品乱码一区二三区的特点| 久久亚洲真实| 日韩中文字幕欧美一区二区| 亚洲一卡2卡3卡4卡5卡精品中文| 成人国产一区最新在线观看| 免费在线观看亚洲国产| 国产精品久久久av美女十八| 欧美另类亚洲清纯唯美| 欧美午夜高清在线| 99热这里只有是精品50| 色综合站精品国产| 国产视频一区二区在线看| 欧美黄色淫秽网站| 长腿黑丝高跟| 国产黄片美女视频| 国产视频内射| 波多野结衣高清作品| 成人国产综合亚洲| 非洲黑人性xxxx精品又粗又长| 久久精品国产清高在天天线| 国产精品亚洲美女久久久| 好男人在线观看高清免费视频| 日韩精品免费视频一区二区三区| 日韩欧美在线乱码| 久久性视频一级片| 国产又色又爽无遮挡免费看| 日日爽夜夜爽网站| 久久精品成人免费网站| 精品久久久久久,| 啦啦啦韩国在线观看视频| 欧美黑人巨大hd| 女人高潮潮喷娇喘18禁视频| 99热这里只有是精品50| 人成视频在线观看免费观看| 神马国产精品三级电影在线观看 | 舔av片在线| 国产一级毛片七仙女欲春2| 亚洲avbb在线观看| 天天添夜夜摸| 动漫黄色视频在线观看| 精品久久久久久成人av| 亚洲人成77777在线视频| 精品国产超薄肉色丝袜足j| 一卡2卡三卡四卡精品乱码亚洲| 久久久久久大精品| 亚洲精品在线美女| 成人三级做爰电影| 亚洲人成77777在线视频| 国产一级毛片七仙女欲春2| www.精华液| 免费看美女性在线毛片视频| 亚洲成人久久性| 亚洲第一电影网av| 搡老妇女老女人老熟妇| 又粗又爽又猛毛片免费看| 黑人欧美特级aaaaaa片| av视频在线观看入口| av天堂在线播放|