本文關(guān)鍵詞：嵌入式周期控制系統(tǒng)的建模與分析　出處：《華東師范大學(xué)》2012年博士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 嵌入式周期控制系統(tǒng) 形式化方法 語義 驗證

【摘要】：嵌入式周期控制系統(tǒng)廣泛應(yīng)用于汽車電子,航空電子等安全攸關(guān)的嵌入式領(lǐng)域.一般來說,這些控制系統(tǒng)都具有周期性行為,它們的共同特點是：(1)以模式為基礎(chǔ).一個周期控制系統(tǒng)由一組模式組成,系統(tǒng)處于一個模式表示系統(tǒng)處于一個特定的狀態(tài).每個模式或是包含若干子模式,或是周期性地進(jìn)行控制計算.(2)面向計算.在一個模式中,周期控制系統(tǒng)會執(zhí)行包含復(fù)雜的計算過程的控制算法.例如,在特點的模式下,一個汽車電子控制系統(tǒng)可以需要處理大量的即時數(shù)據(jù),以便確定車輛的位置和姿態(tài).(3)周期性.周期控制系統(tǒng)是一個反應(yīng)式系統(tǒng),可能會連續(xù)運(yùn)行很長一段時間.每個模式的行為由其自身的周期決定.因此,大部分的計算任務(wù)都是在一個周期內(nèi)完成的.如果沒有發(fā)生模式切換,那么這些計算任務(wù)還將在下一個周期再次執(zhí)行.在周期結(jié)束時,如果滿足特定的條件,系統(tǒng)將從當(dāng)前模式轉(zhuǎn)入其它模式. 盡管這類系統(tǒng)被廣泛地應(yīng)用于航天／航空,汽車電子等安全攸關(guān)的嵌入式領(lǐng)域,但是工業(yè)界仍然缺少一種針對這一領(lǐng)域的形式化建模語言.我們曾對現(xiàn)有的建模語言做過廣泛的調(diào)研,這些語言或是較為復(fù)雜,使用門檻較高,或是過于通用,難以處理這類系統(tǒng)的特征.因此,我們根據(jù)領(lǐng)域工程師的需求,設(shè)計了SPARDL建模框架.該框架主要包括兩個部分,第一部分是作為建模標(biāo)記的模式圖(ModeDiagram),第二部分是規(guī)范語言SPRL. 模式圖是以經(jīng)典的狀態(tài)圖(Statecharts)[56]為基礎(chǔ),增加了支持周期控制系統(tǒng)建模的特殊領(lǐng)域需求的建模標(biāo)記.模式圖的核心部分是一組模式.每個模式都有特點的周期長度.不同的模式的周期可以不同.在周期結(jié)束時,如果滿足一定的條件,將發(fā)生模式切換.允許模式嵌套,也允許模式-子模式之間發(fā)生切換.與其它建模語言相比,SPARDL的特色之一是模式之間的遷移條件是可以涉及歷史狀態(tài)的時序表達(dá)式. 模式圖的結(jié)構(gòu)是層次化的,分為模式-控制流-模塊三個層次.一個模式既可以包含若干子模式,也可以包含一個控制流.控制流是特定的控制算法,計算任務(wù)的封裝.控制流的細(xì)節(jié)在控制流層面表述.允許在控制流中調(diào)用模塊,模塊的細(xì)節(jié)在模式層展示. 為了支持模式圖的形式化推理,SPARDL框架還包括基于區(qū)段演算[42]的規(guī)范語言.該語言適于描述領(lǐng)域工程師關(guān)心的時序性質(zhì). SPARDL模型的正確性取決于它的模式圖是否滿足規(guī)范.由于SPARDL模型可能涉及到復(fù)雜的非線性運(yùn)算,因此,完整的驗證是不可行的.為了解決這個問題,本文利用概率模型檢查技術(shù)[125,126]驗證SPARDL模型.試驗結(jié)果表明,本文的方法學(xué)能夠發(fā)現(xiàn)真實系統(tǒng)中的設(shè)計錯誤. 本文主要有下列貢獻(xiàn)： ●提出了新的形式化建�？蚣躍PARDL,該框架的主要目的是為嵌入式周期控制程序提供一套清晰而準(zhǔn)確的建模機(jī)制. ●通過兩種方式研究了SPARDL的形式化語義,一是將SPARDL模型解釋為價格時間自動機(jī)(Priced Timed Automata),二是在遷移系統(tǒng)上定義它的操作語義.在操作語義的基礎(chǔ)上討論了SPARDL的類型安全,互模擬,等價等問題. ●在形式化語義的基礎(chǔ)上,實現(xiàn)了SPARDL的仿真.并擴(kuò)展了最初的操作語義,提出了SPARDL的概率語義.根據(jù)新的概率語義,開發(fā)了以仿真為基礎(chǔ)的概率模型檢查,用于驗證SPARDL模型是否滿足各種時序性質(zhì). ●在真實的案例中試用了SPARDL眶架,發(fā)現(xiàn)了一個控制系統(tǒng)中的兩個真實的缺陷.試用結(jié)果充分說明了SPARDL的有效性.
[Abstract]:Embedded cycle control system is widely used in automotive electronics, embedded field of aviation electronic safety. In general, these control systems have periodic behavior, their common features are: (1) to pattern based. One cycle control system consists of a set of patterns, the system is in a mode of the system is a particular state. Each mode is or contains a number of sub models, or periodically control calculation. (2) for computing. In one mode, the control algorithm of cycle control system will perform the calculation process includes complex. For example, the characteristics of the model, a vehicle electronic control the system can deal with the immediate needs a large amount of data, in order to determine the position and attitude of the vehicle. (3) a periodic cycle. The control system is a reactive system, may run continuously for a long period of time for each mode. On the grounds of its own cycle decision. Therefore, most computing tasks are completed in a period. If there was no mode switching, so these tasks will be in the next cycle is executed again. At the end of the cycle, if satisfy certain conditions, the system will be transferred to other modes from the current mode.
Although this type of system is widely used in aerospace and aviation, automotive electronics and other fields of embedded security at stake, but the industry still lacks a formal modeling language in this field. We have the existing modeling languages have done extensive research, these languages or more complex, with a higher threshold, or is too general, characteristics of difficult to deal with this kind of system. Therefore, we according to the field engineer needs to design the SPARDL modeling framework. The framework mainly includes two parts, the first part is as a model graph modeling marker (ModeDiagram), the second part is the specification language SPRL.
Model mapping is a state diagram of the classic (Statecharts) [56] based modeling markup special field demand control system modeling support cycle. The core part of the pattern is a set of mode. Each mode has the characteristics of cycle length. Different periodic patterns can not the same. At the end of the cycle, if meet certain conditions, will allow the mode switch. Nested mode also allows, between sub mode switching mode. Compared with other modeling language, one of the features of SPARDL is the migration conditions between the modes is temporal expressions can relates to historical state.
The diagram is hierarchical, divided into model control flow module three levels. A model can contain several sub models, can also include a control flow control flow control algorithm is given. The calculation task package. Details of the control flow in the control flow level allowed in the statement. The control flow in the calling module, display module details in the model layer.
In order to support formal reasoning of schema diagrams, the SPARDL framework also includes a specification language based on section calculus [42]. This language is suitable for describing the timing properties of domain engineers.
Right depends on the mode of the SPARDL map in it whether meet the specifications. The SPARDL model may involve complicated nonlinear operation, therefore, the complete verification is not feasible. In order to solve this problem, this paper using [125126] probability model checking the SPARDL model. The experimental results show that this method can find the design the error in the real system.
The main contributions of this article are as follows:
A new formalized modeling framework (SPARDL) is proposed. The main purpose of the framework is to provide a clear and accurate modeling mechanism for the embedded cycle control program.
The formal semantics of SPARDL is studied by two ways, one is the SPARDL model to explain the price for the automaton (Priced Timed Automata) time, two is the definition of its operational semantics in the migration system. The operational semantics based on discussion of SPARDL type safety, bisimulation equivalence, and other issues.
In the basis of the formal semantics, SPARDL realized the simulation. And expanded the original operational semantics, probabilistic semantic SPARDL. According to the new development of the probabilistic semantics, probability model checking based on simulation, SPARDL model is used to verify whether meet the various temporal properties.
The SPARDL orbital frame was tested in a real case, and two real defects in a control system were found. The trial results fully illustrate the effectiveness of the SPARDL.

【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2012
【分類號】：TP368.1;TP273

【共引文獻(xiàn)】

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

1 王雷;陳歸;金茂忠;;基于約束分析與模型檢測的代碼安全漏洞檢測方法研究[J];計算機(jī)研究與發(fā)展;2011年09期

2 李仁見;王昭飛;;命令式程序終止性驗證方法綜述[J];計算機(jī)工程與應(yīng)用;2011年28期

3 林夢香;吳國仕;;程序模型檢查器綜述[J];計算機(jī)科學(xué);2009年04期

4 張志;張林;曾慶凱;;改進(jìn)的程序時序安全屬性模型檢測技術(shù)[J];計算機(jī)工程;2011年07期

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

1 李仁見;堆操作程序分析驗證技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2011年

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

3 王振明;用于指針邏輯的自動定理證明器的設(shè)計與實現(xiàn)[D];中國科學(xué)技術(shù)大學(xué);2009年

4 劉萬偉;擴(kuò)展時序邏輯的推理及符號化模型檢驗技術(shù)[D];國防科學(xué)技術(shù)大學(xué);2009年

5 胡斌;可信的自治式服務(wù)協(xié)同系統(tǒng)驗證[D];浙江大學(xué);2009年

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

1 劉自恒;循環(huán)不變式生成方法研究與改進(jìn)[D];南京大學(xué);2012年

，

本文編號：1375946