[發(fā)明專利]基于著色Petri網(wǎng)能力使命線程形式描述與驗證方法

有效

• 申請?zhí)枺?/td>: 201710171811.1
• 申請日: 2017-03-22
• 公開（公告）號: CN106997411B
• 公開（公告）日: 2020-09-29
• 發(fā)明（設(shè)計）人: 陶智剛;蔣飛;蔣鍇;任志宏;孔俊俊;徐浩
• 申請（專利權(quán)）人: 中國電子科技集團(tuán)公司第二十八研究所
• 主分類號: G06F30/22
• 分類號: G06F30/22
• 代理公司: 南京蘇高專利商標(biāo)事務(wù)所(普通合伙) 32204
• 代理人: 柏尚春

本發(fā)明公開了一種基于著色Petri網(wǎng)能力使命線程形式描述與驗證方法。描述使命線程中的邏輯關(guān)系及活動規(guī)則；引入同步器對邏輯關(guān)系進(jìn)行形式化，并建立帶環(huán)同步網(wǎng)；基于帶環(huán)同步網(wǎng)建立使命線程邏輯模型；建立活動規(guī)則與CPN之間的轉(zhuǎn)換關(guān)系，從而基于使命線程邏輯模型構(gòu)建使命線程語義模型；基于使命線程語義模型的暢通性和一致性提出兩個驗證準(zhǔn)則；在使命線程語義模型中加入時間動態(tài)進(jìn)行擴(kuò)展，得到混雜使命線程模型，進(jìn)行仿真分析并獲取屬性值。本發(fā)明提出了形式化描述能力使命線程的使命線程語義模型，避免其它線程建模語言在使命線程形式化建模與分析驗證上的不足；支持復(fù)雜的仿真分析和獲取使命線程的屬性值，能夠支撐體系的評估。

技術(shù)領(lǐng)域

本發(fā)明屬于體系結(jié)構(gòu)驗證領(lǐng)域，尤其涉及一種基于著色Petri網(wǎng)能力使命線程形式描述與驗證方法。

背景技術(shù)

作戰(zhàn)概念(concept of operations,CONOPS)描述了特定的一組活動是如何得到執(zhí)行的，且執(zhí)行這些活動的本領(lǐng)依賴于許多因素以及這些因素間內(nèi)在的相互關(guān)聯(lián)。能力可以由一個或多個使命線程來描述，而使命線程(mission thread)通常定義為“一組操作活動，活動的執(zhí)行順序及與時間相關(guān)的屬性，以及為完成活動所需要的信息”。通過建立能力與作戰(zhàn)活動的映射關(guān)系，可建立能力分析和作戰(zhàn)活動分析之間的橋梁，并識別作戰(zhàn)活動是如何使用各種可獲得的能力元素來得以實現(xiàn)的；它也可用于追溯作戰(zhàn)活動是如何滿足能力需求的。而描述使命線程的一組作戰(zhàn)活動可被看作是使命領(lǐng)域體系結(jié)構(gòu)的基礎(chǔ)，而體系結(jié)構(gòu)提供了一個結(jié)構(gòu)來定義和理解影響體系能力的許多復(fù)雜因素。

使命線程可通過執(zhí)行、信息、屬性三個維度來描述和表達(dá)。執(zhí)行維規(guī)定了使命線程應(yīng)該執(zhí)行的活動以及活動間的關(guān)系。信息維規(guī)定了活動輸入/輸出所需要的信息。屬性維規(guī)定了使命線程所描述的能力所需的屬性，屬性值的獲取一般需要通過仿真和統(tǒng)計分析來獲得。

目前，關(guān)于使命線程的建模語言有BPMN、IDEF3、活動圖、用例圖和信息流圖等。但是這些建模語言缺乏形式化的模型和手段來對使命線程進(jìn)行分析和驗證。通常，使命線程合理的形式化模型應(yīng)該擁有如下的四個性質(zhì)：(1)具有自動執(zhí)行的語義，并且語義能被嚴(yán)格地形式定義，從而使得模型能被計算機(jī)執(zhí)行；(2)能如實地代表使命線程，“如實性(faithfulness)”意味著使命線程形式化模型和使命線程之間通過一個可檢驗的語義保持來相互關(guān)聯(lián)，換句話說，使命線程形式模型任何可被驗證的性質(zhì)在使命線程中都將保持不變；(3)能支持形式化的分析和驗證，通過開發(fā)可擴(kuò)展的算法，使命線程的行為特性能被檢驗；(4)可擴(kuò)展，從而支持性能分析，比如，時間和概率可以加入到使命線程的形式模型中，使命線程的屬性值可以通過仿真和統(tǒng)計分析得到。

發(fā)明內(nèi)容

發(fā)明目的：常用的BPMN、IDEF3、活動圖、用例圖和信息流圖等使命線程建模語言往往缺乏形式化的模型和技術(shù)，無法對所建立的使命線程模型進(jìn)行形式分析和驗證，具體表現(xiàn)在模型無法形式化、缺乏自動執(zhí)行語義導(dǎo)致無法被計算機(jī)自動執(zhí)行、缺乏形式驗證算法和手段、不支持性能分析等，為了避免以上建模語言的不足，本發(fā)明提出一種基于著色Petri網(wǎng)能力使命線程形式描述與驗證方法。

技術(shù)方案：一種基于著色Petri網(wǎng)能力使命線程形式描述與驗證方法，包括以下步驟：

(1)提供使命線程的信息表，根據(jù)信息表在活動間的傳遞過程，梳理分析使命線程中活動關(guān)系，包括活動與活動之間的關(guān)系即邏輯關(guān)系，以及活動輸入輸出間的關(guān)系即活動規(guī)則；

(2)為形式化描述使命線程中的邏輯關(guān)系，引入同步器，并建立邏輯關(guān)系與同步器之間的轉(zhuǎn)換關(guān)系，建立由同步器與庫所/變遷系統(tǒng)這樣一類普通Petri網(wǎng)組合而成的帶環(huán)同步網(wǎng)；基于帶環(huán)同步網(wǎng)，給出使命線程邏輯的形式定義和執(zhí)行規(guī)則，建立使命線程邏輯模型；