【摘要】：隨著網(wǎng)絡(luò)技術(shù)的不斷發(fā)展,物聯(lián)網(wǎng)／物理信息融合系統(tǒng)成為目前研究和發(fā)展的熱點。一個典型的例子是智能交通系統(tǒng)(ITS)。通信作為信息交換的媒介,已成為物聯(lián)網(wǎng)研究的核心問題之一。在智能交通系統(tǒng)中,車輛可以與服務(wù)中心溝通(V2I),告知其他車輛他們的存在以便于車輛的安全監(jiān)控和安全駕駛；另外車輛和車輛之間也可以通信(V2V),從而提高交通的安全性,避免惡性交通事故的發(fā)生。 該系統(tǒng)通信的實時性研究是非常重要的。分布式的系統(tǒng)通信更強(qiáng)調(diào)邏輯時鐘。為此本論文提出一種新型的適用于分布式系統(tǒng)通信的時間化網(wǎng)絡(luò)通信模型(Timed-pNets)。該模型包括了刻畫時間化動作(Time Action)的邏輯時鐘(Logical Clock)、時間化規(guī)范(Timed Specification)、時間參數(shù)化標(biāo)簽遷移系統(tǒng)(timed Parameterized Label Transition System,timed-pLTS)等基本構(gòu)件。Timed-pNets是樹型分層結(jié)構(gòu)模型,其葉子節(jié)點由Timed-pLTS表述,非葉子節(jié)點是子網(wǎng)的抽象,用于同步子網(wǎng)之間的通信。本論文的主要貢獻(xiàn)如下： ·建立了一個分布式具有同步和異步通信的時間化模型Timed-pNets。在引入時間化動作形成動作邏輯時鐘基礎(chǔ)上,建立時間化的pLTS系統(tǒng)(Timed-pLTS)。Timed-pLTS中的標(biāo)簽為邏輯時鐘,用于觸發(fā)系統(tǒng)從一個狀態(tài)遷移到另一個狀態(tài)。論文把信道設(shè)計為Timed-pLTS,具有信息接受和發(fā)送兩個動作邏輯時鐘,用來描述異步通信。基于Timed-pLTS,論文構(gòu)造了Timed-pNets模型,它的同步向量用于描述不同節(jié)點之間的同步通信。研究Timed-pNets的相容性(Compatibility)和延遲性(Delay)。 ·提出了時間規(guī)范(Timed Specication)的概念。時間規(guī)范定義為一組邏輯時鐘和這些時鐘上的關(guān)系,包括時鐘優(yōu)先關(guān)系和時鐘同步關(guān)系。提出了時鐘劃分和時鐘合并的概念以簡化時間規(guī)范,研究了時鐘的優(yōu)先關(guān)系和同步關(guān)系作用在劃分后時鐘上的語義。 ·設(shè)計了一組算法用于把Timed-pLTS和Timed-pNets轉(zhuǎn)化為時間規(guī)范,并提出了一套利用時間規(guī)范來建立層次化模型的理論和方法。這樣人們可以靈活地設(shè)計通信系統(tǒng)：既可以先設(shè)計葉子節(jié)點,然后組合成Timed-pNets節(jié)點這種層層向上的方法構(gòu)建系統(tǒng),也可以先設(shè)計一個抽象的Timed-pNets系統(tǒng),然后用具體的Timed-pLTS實例化該系統(tǒng)中每個抽象孔的由上至下方式構(gòu)建系統(tǒng)。 ●以智能交通系統(tǒng)中車輛相互通信為例子,實現(xiàn)如何建立Timed-pNets模型,以及檢查通信的安全性和時間性質(zhì)。使用TimeSquare工具完成這些性質(zhì)的測試,結(jié)果表明論文建立的timed-pNets具有通用性和靈活性。
[Abstract]:With the continuous development of network technology, the Internet of things / physical information fusion system has become a hot research and development. A typical example is the Intelligent Transportation system (ITS).) As the medium of information exchange, communication has become one of the core problems in the research of Internet of things. In its, vehicles can communicate with service centres (V2I) to inform other vehicles of their presence to facilitate vehicle safety monitoring and safe driving, and can also communicate with vehicles (V2V) to improve traffic safety. Avoid serious traffic accidents. It is very important to study the real-time communication of this system. Distributed system communication places more emphasis on logical clocks. In this paper, a new time network communication model (Timed-pNets) for distributed system communication is proposed. The model includes the logical clock (Logical Clock), time specification, (Timed Specification), time parameterized label migration system, (timed Parameterized Label Transition system timed-pLTS, and other basic components. Timed-pNets is a tree hierarchical structure model, the leaf nodes of which are expressed by Timed-pLTS. A non-leaf node is an abstraction of a subnet and is used to synchronize communication between subnets. The main contributions of this thesis are as follows: a distributed Timed-pNets model with synchronous and asynchronous communication is proposed. Based on the introduction of temporal action to form action logical clock, the label in the timed pLTS system (Timed-pLTS) .Timed-pLTS is established as the logical clock, which is used to trigger the system to migrate from one state to another. In this paper, the channel is designed as Timed-pLTS, which has two action logic clocks, message receiving and transmitting, which are used to describe asynchronous communication. Based on Timed-pLTS, this paper constructs a Timed-pNets model, whose synchronization vector is used to describe the synchronous communication between different nodes. The concept of time gauge (Timed Specication) is proposed to study the compatibility of Timed-pNets with (Compatibility) and delay (Delay). Time specification is defined as the relationship between a set of logical clocks and these clocks, including clock precedence and clock synchronization. In this paper, the concepts of clock division and clock merging are proposed to simplify the time specification, and the semantics of clock precedence and synchronization relationship are studied. A set of algorithms are designed to transform Timed-pLTS and Timed-pNets into time specification. A set of theories and methods for building hierarchical models using time specification are presented. In this way, people can design communication systems flexibly: they can design leaf nodes first, then combine them into Timed-pNets nodes to build up the system layer by layer, or they can design an abstract Timed-pNets system first. Then we use the concrete Timed-pLTS to instantiate each abstract hole in the system to construct the system from top to bottom. Taking the communication between vehicles in the intelligent transportation system as an example, how to establish the Timed-pNets model is realized. And check the security and time nature of the communication. The TimeSquare tool is used to complete the test of these properties. The results show that the timed-pNets established in this paper is universal and flexible.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2014
【分類號】：TN915.01

【共引文獻(xiàn)】

相關(guān)期刊論文 前10條

1 史永勝;李建雪;;基于模糊Petri網(wǎng)的維修保障活動可視化建模與仿真研究[J];飛機(jī)設(shè)計;2013年06期

2 莫晶;;空管自動化系統(tǒng)中一種多副本數(shù)據(jù)同步的設(shè)計與實現(xiàn)[J];福建電腦;2014年05期

3 李俊;王賢琳;;基于分解法建模的泵送系統(tǒng)可靠性和可用性評估[J];工程設(shè)計學(xué)報;2015年01期

4 馮輝寧;;組合計算模型實現(xiàn)系統(tǒng)設(shè)計與仿真[J];計算機(jī)應(yīng)用研究;2010年06期

5 李磊;錢彥嶺;楊擁民;杜凱;;基于概率模型檢驗的復(fù)雜武器系統(tǒng)任務(wù)可靠性評估方法研究[J];機(jī)械工程學(xué)報;2011年24期

6 劉通;王鳳英;;基于OPM的安全起源模型[J];計算機(jī)應(yīng)用研究;2013年10期

7 羅軍;王宏;李文生;;基于向量時鐘模型的NoSQL最終一致性的研究[J];計算機(jī)工程與應(yīng)用;2013年23期

8 楊曉松;武小悅;;基于DSPN的航天測控系統(tǒng)任務(wù)可靠性仿真建模[J];航空動力學(xué)報;2014年01期

9 袁春陽;許俊峰;朱春鴿;;一種可確保完整性策略有效性的可信恢復(fù)模型[J];計算機(jī)研究與發(fā)展;2014年02期

10 張晶;潘有順;;嵌入式系統(tǒng)同步進(jìn)程的競態(tài)條件分析與推理學(xué)習(xí)方法[J];計算機(jī)科學(xué);2014年02期

相關(guān)會議論文 前1條

1 王學(xué)慧;張磊;方糧;;復(fù)雜系統(tǒng)仿真中時間管理技術(shù)研究綜述[A];系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)論文集（第15卷）[C];2014年

相關(guān)博士學(xué)位論文 前10條

1 王兵;邏輯進(jìn)程范型的形式語義、算法評估及其在空間隨機(jī)仿真中的應(yīng)用[D];國防科學(xué)技術(shù)大學(xué);2011年

2 張晉津;轉(zhuǎn)換系統(tǒng)行為近似等價性的研究[D];南京航空航天大學(xué);2010年

3 祝義;嵌入式軟件需求規(guī)約到軟件體系結(jié)構(gòu)模型的轉(zhuǎn)換研究[D];南京航空航天大學(xué);2011年

4 劉志鋒;模型檢測中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

5 竇連旺;網(wǎng)絡(luò)控制系統(tǒng)的建模、穩(wěn)定性分析及其調(diào)度的研究[D];天津大學(xué);2004年

6 賈文崢;大型鐵路客運站的進(jìn)路分配問題及緩沖時間研究[D];北京交通大學(xué);2010年

7 朱素霞;面向多核處理器確定性重演的內(nèi)存競爭記錄機(jī)制研究[D];哈爾濱工業(yè)大學(xué);2013年

8 周侃;高鐵客運樞紐換乘行為分析與設(shè)施配置方法研究[D];哈爾濱工業(yè)大學(xué);2013年

9 毛華堅;云環(huán)境中的移動文件存儲和時空數(shù)據(jù)分析關(guān)鍵技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2013年

10 劉光輝;高效處理器容錯技術(shù)研究與實現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2013年

相關(guān)碩士學(xué)位論文 前10條

1 何嘉林;面向“執(zhí)行體”的實時交通控制系統(tǒng)建模與執(zhí)行策略研究[D];昆明理工大學(xué);2010年

2 沈嘉權(quán);IF對實時軟件設(shè)計圖形模型的驗證[D];昆明理工大學(xué);2009年

3 劉志遠(yuǎn);基于密鑰鏈的認(rèn)證郵件協(xié)議的擴(kuò)展及形式化驗證[D];山東大學(xué);2011年

4 張穎;基于博弈的多參與者合同簽署協(xié)議的驗證[D];山東大學(xué);2010年

5 楊柳倩;基于UML和有色Petri網(wǎng)的RBC切換建模與分析[D];蘭州交通大學(xué);2012年

6 仵志科;基于事件的信息物理系統(tǒng)時空建模研究[D];華東師范大學(xué);2013年

7 軒瑤;基于電子商務(wù)平臺的鐵路車站整車貨物作業(yè)流程優(yōu)化研究[D];北京交通大學(xué);2013年

8 劉通;基于OPM的安全起源研究[D];山東理工大學(xué);2013年

9 潘隆濤;新型墻材生產(chǎn)過程管理系統(tǒng)的開發(fā)[D];南昌大學(xué);2013年

10 段皓;基于CUDA的JPEG-LS編碼器的并行設(shè)計[D];西北農(nóng)林科技大學(xué);2013年

，

本文編號：2185213