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

【摘要】：形式化方式包括了形式規(guī)范和設(shè)計(jì)驗(yàn)證兩個(gè)方面，它的目的是以數(shù)學(xué)的方式來(lái)對(duì)系統(tǒng)進(jìn)行描述，，為保證軟件的可靠性提供條件。在現(xiàn)代軟件系統(tǒng)開(kāi)發(fā)過(guò)程當(dāng)中，經(jīng)常會(huì)要求在某些限定的時(shí)間約束之下，對(duì)系統(tǒng)的輸入數(shù)據(jù)進(jìn)行相應(yīng)的處理，以及系統(tǒng)內(nèi)部所進(jìn)行的狀態(tài)之間的變遷，最后給出對(duì)應(yīng)的輸出數(shù)據(jù)。 本文的主要工作如下： 本文首先介紹了一種結(jié)合接口自動(dòng)機(jī)（Interface Automata）和Z語(yǔ)言的規(guī)范ZIA以及ZIAs之間的精化關(guān)系。然后研究了MARTE（Modeling and Analysis of Real-Time andEmbedded Systems），它在UML的基礎(chǔ)上對(duì)于時(shí)間以及其他方面進(jìn)行了一定的擴(kuò)充。MARTE定義了基于模型的實(shí)時(shí)和嵌入式系統(tǒng)描述的基礎(chǔ)。本文詳細(xì)描述了MARTE中的一些基本和核心概念。然后給出了一種基于離散時(shí)間的ZIA模型規(guī)范（DT-ZIA），它不僅能夠描述某些實(shí)時(shí)系統(tǒng)中針對(duì)在離散時(shí)間下的時(shí)間約束的要求，同時(shí)能夠?qū)ο到y(tǒng)的數(shù)據(jù)處理和狀態(tài)變遷進(jìn)行精確的表達(dá)。接著是MARTE的六元組表示，再接著是MARTE到DT-ZIA的轉(zhuǎn)換方法。最后我們給出了在有限定義域上的ZIAs精化檢測(cè)算法（包括算法的數(shù)據(jù)結(jié)構(gòu)和流程圖）、面向帶有數(shù)據(jù)約束的實(shí)時(shí)系統(tǒng)的時(shí)序邏輯和在有限定義域上的DT-ZIA模型檢測(cè)算法（包括實(shí)現(xiàn)類圖和流程圖）以及兩個(gè)算法的實(shí)例驗(yà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é)位級(jí)別】：碩士
【學(xué)位授予年份】：2012
【分類號(hào)】：TP334.7;TP301.1

【共引文獻(xiàn)】

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

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

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

本文編號(hào)：1553191