本文關(guān)鍵詞：STALLOY：一種時(shí)空建模與分析語言　出處：《華東師范大學(xué)》2017年碩士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： Alloy語言 空間邏輯 時(shí)態(tài)邏輯 時(shí)空邏輯 STALLOY 列車控制系統(tǒng)

【摘要】：Alloy是一種形式化建模語言,它采用模型驅(qū)動(dòng)式的開發(fā)方法,對(duì)目標(biāo)系統(tǒng)進(jìn)行形式化的建模與分析,解決了傳統(tǒng)軟件開發(fā)中使用非形式化語言描述軟件規(guī)格帶來的矛盾性、二義性以及模糊性等問題,并揭露了系統(tǒng)設(shè)計(jì)中存在的錯(cuò)誤和缺陷,為我們提供了一個(gè)需求明確、結(jié)構(gòu)良好的軟件框架。在現(xiàn)實(shí)物理系統(tǒng)的建模與分析中,我們不可避免的會(huì)遇到時(shí)間、空間性質(zhì)描述的需求,但是,Alloy中缺乏了時(shí)間、空間概念的定義,這使得我們無法使用Alloy進(jìn)行時(shí)空相關(guān)系統(tǒng)的建模與分析。因此,如何在Alloy的基礎(chǔ)上構(gòu)建出一個(gè)具有時(shí)空建模能力的語言顯得尤為迫切。在時(shí)空性質(zhì)的表示與推理中,空間邏輯提供了一組關(guān)系用來描述和判定對(duì)象之間是否存在某種空間上的聯(lián)系;時(shí)態(tài)邏輯提供了一系列時(shí)態(tài)操作符來描述目標(biāo)系統(tǒng)中時(shí)間相關(guān)的動(dòng)作。本文通過對(duì)Alloy語言以及空間、時(shí)間邏輯的研究與分析,提出了一種時(shí)空建模與分析語言STALLOY,主要構(gòu)建過程包括:1)基于Alloy語言以及空間、時(shí)態(tài)邏輯的特點(diǎn),構(gòu)造了符合Alloy語言規(guī)范的空間操作符和時(shí)態(tài)操作符,通過將它們作用到空間原子變量區(qū)域上,來產(chǎn)生用于時(shí)空推理與演算的空間變量集合;2)將區(qū)域演算理論與空間操作符結(jié)合,構(gòu)建了一組空間關(guān)系用來表示空間區(qū)域或區(qū)域項(xiàng)之間是否存在某種空間上的聯(lián)系,同時(shí)將時(shí)態(tài)操作符引入一階布爾邏輯公式來描述時(shí)間相關(guān)的性質(zhì);3)對(duì)Alloy的一階關(guān)系邏輯進(jìn)行擴(kuò)展,加入構(gòu)造的時(shí)態(tài)、空間操作符和關(guān)系,構(gòu)建了時(shí)空建模與分析語言STALLOY,并根據(jù)拓?fù)鋾r(shí)空模型給出了它的語法和語義;4)經(jīng)過分析,給出了STALLOY的時(shí)空邏輯的計(jì)算復(fù)雜度是EXPSPACE完全的證明,并應(yīng)用它對(duì)時(shí)空系統(tǒng)中若干性質(zhì)進(jìn)行了描述。在構(gòu)建了STALLOY語言后,我們給出了它的工具實(shí)現(xiàn),其中包括:1)基于拓?fù)潢P(guān)系數(shù)據(jù)模型,我們將空間區(qū)域抽象為拓?fù)涠噙呅?并據(jù)此給出了空間操作符的實(shí)現(xiàn)算法,同時(shí)結(jié)合Alloy語言給出了空間關(guān)系的實(shí)現(xiàn);2)在構(gòu)建了STALLOY時(shí)序關(guān)系的基礎(chǔ)上,實(shí)現(xiàn)了時(shí)態(tài)操作符以及時(shí)態(tài)關(guān)系;3)將STALLOY時(shí)空邏輯的實(shí)現(xiàn)應(yīng)用到Alloy開源工具中構(gòu)造出了 STALLOY的工具。本文最后以列車防護(hù)系統(tǒng)為例,通過應(yīng)用STALLOY及其工具對(duì)系統(tǒng)進(jìn)行時(shí)空建模、分析和驗(yàn)證,展示了 STALLOY進(jìn)行時(shí)空系統(tǒng)建模與分析的能力。
[Abstract]:Alloy is a formal modeling language, which uses model-driven development method to model and analyze the target system. It solves the problems of contradiction ambiguity and fuzziness caused by the use of non-formal language in the traditional software development and exposes the errors and defects in the system design. It provides us with a well-structured software framework. In the modeling and analysis of real physical systems, we will inevitably meet the need to describe the properties of time and space, but. There is no definition of time and space in Alloy, which makes it impossible for us to use Alloy to model and analyze space-time related systems. How to build a language with the ability of spatiotemporal modeling on the basis of Alloy is particularly urgent, in the representation and reasoning of space-time properties. Spatial logic provides a set of relationships to describe and determine whether there is a spatial relationship between objects; Temporal logic provides a series of temporal operators to describe the time-related actions in the target system. This paper studies and analyzes the Alloy language and spatial and temporal logic. A spatiotemporal modeling and analysis language (STALLOY) is proposed. The main construction process includes: 1) based on Alloy language and the characteristics of spatial and temporal logic. The spatial and temporal operators, which conform to Alloy specification, are constructed to generate the set of spatial variables for spatio-temporal reasoning and calculus by applying them to the region of spatial atomic variables. 2) combining regional calculus theory with spatial operators, a set of spatial relationships are constructed to indicate whether there is a spatial relationship between spatial regions or regional items. At the same time, the temporal operator is introduced into the first-order Boolean logic formula to describe the time-dependent properties. 3) extend the first-order relational logic of Alloy, add the constructed tenses, spatial operators and relations, and construct the spatiotemporal modeling and analysis language STALLOY. The syntax and semantics are given according to the topological space-time model. 4) after analysis, the computational complexity of STALLOY's space-time logic is proved completely by EXPSPACE. It is used to describe some properties of space-time system. After constructing STALLOY language, we give its tool implementation, which includes: 1) data model based on topological relation. The spatial region is abstracted into topological polygon, and the realization algorithm of spatial operator is given based on it, and the realization of spatial relation is given with Alloy language. 2) on the basis of constructing STALLOY temporal relation, the temporal operator and temporal relation are realized. 3) the realization of STALLOY space-time logic is applied to Alloy open source tool to construct the tool of STALLOY. Finally, this paper takes the train protection system as an example. By using STALLOY and its tools to model, analyze and verify the system, the ability of STALLOY to model and analyze the spatio-temporal system is demonstrated.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP311.52

【參考文獻(xiàn)】

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

1 董凱霞;劉曉娟;朱耘燕;;城市軌道交通CBTC系統(tǒng)車載ATP仿真研究[J];鐵道通信信號(hào);2011年04期

，

本文編號(hào)：1385195