本文關(guān)鍵詞： MARTE 離散時間自動機(jī) 接口自動機(jī) Z語言 模型檢測　出處：《南京航空航天大學(xué)》2012年碩士論文　論文類型：學(xué)位論文

【摘要】：形式化方式包括了形式規(guī)范和設(shè)計驗證兩個方面，它的目的是以數(shù)學(xué)的方式來對系統(tǒng)進(jìn)行描述，，為保證軟件的可靠性提供條件。在現(xiàn)代軟件系統(tǒng)開發(fā)過程當(dāng)中，經(jīng)常會要求在某些限定的時間約束之下，對系統(tǒng)的輸入數(shù)據(jù)進(jìn)行相應(yīng)的處理，以及系統(tǒng)內(nèi)部所進(jìn)行的狀態(tài)之間的變遷，最后給出對應(yīng)的輸出數(shù)據(jù)。 本文的主要工作如下： 本文首先介紹了一種結(jié)合接口自動機(jī)（Interface Automata）和Z語言的規(guī)范ZIA以及ZIAs之間的精化關(guān)系。然后研究了MARTE（Modeling and Analysis of Real-Time andEmbedded Systems），它在UML的基礎(chǔ)上對于時間以及其他方面進(jìn)行了一定的擴(kuò)充。MARTE定義了基于模型的實時和嵌入式系統(tǒng)描述的基礎(chǔ)。本文詳細(xì)描述了MARTE中的一些基本和核心概念。然后給出了一種基于離散時間的ZIA模型規(guī)范（DT-ZIA），它不僅能夠描述某些實時系統(tǒng)中針對在離散時間下的時間約束的要求，同時能夠?qū)ο到y(tǒng)的數(shù)據(jù)處理和狀態(tài)變遷進(jìn)行精確的表達(dá)。接著是MARTE的六元組表示，再接著是MARTE到DT-ZIA的轉(zhuǎn)換方法。最后我們給出了在有限定義域上的ZIAs精化檢測算法（包括算法的數(shù)據(jù)結(jié)構(gòu)和流程圖）、面向帶有數(shù)據(jù)約束的實時系統(tǒng)的時序邏輯和在有限定義域上的DT-ZIA模型檢測算法（包括實現(xiàn)類圖和流程圖）以及兩個算法的實例驗證。
[Abstract]:The formal method includes formal specification and design verification. Its purpose is to describe the system in a mathematical way and to provide conditions for ensuring the reliability of software. It is often required to deal with the input data of the system and the transitions between states within the system under some limited time constraints. Finally, the corresponding output data are given. The main work of this paper is as follows:. In this paper, we first introduce a refined relation between ZIA and ZIAs, which combines interface automata with Z language. Then we study the MARTE(Modeling and Analysis of Real-Time andEmbedded Systems swarms. Based on UML, we study time and other aspects. In this paper, some basic and core concepts in MARTE are described in detail. Then, a discrete time based ZIA model specification is given. Can only describe the requirements of some real-time systems for time constraints in discrete time, At the same time, it can accurately express the data processing and state transition of the system. Then there is the six-tuple representation of MARTE. Finally, we give the ZIAs refinement detection algorithm on the finite domain, including the data structure and flowchart of the algorithm, the temporal logic of the real-time system with data constraints and. The DT-ZIA model checking algorithm (including class diagram and flowchart) on the finite domain and the verification of two algorithms are given.
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2012
【分類號】：TP334.7;TP301.1

【共引文獻(xiàn)】

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

1 賀志宏;曾慶凱;;基于SPIN的LTL屬性分解方法研究[J];計算機(jī)應(yīng)用與軟件;2014年07期

2 秦曉軍;甘水滔;陳左寧;;一種基于一階邏輯的軟件代碼安全性缺陷靜態(tài)檢測技術(shù)[J];中國科學(xué):信息科學(xué);2014年01期

本文編號：1553191