STALLOY：一种时空建模与分析语言

发布时间：2018-01-05 23:01

本文关键词：STALLOY：一种时空建模与分析语言　出处：《华东师范大学》2017年硕士论文　论文类型：学位论文

【摘要】：Alloy是一种形式化建模语言,它采用模型驱动式的开发方法,对目标系统进行形式化的建模与分析,解决了传统软件开发中使用非形式化语言描述软件规格带来的矛盾性、二义性以及模糊性等问题,并揭露了系统设计中存在的错误和缺陷,为我们提供了一个需求明确、结构良好的软件框架。在现实物理系统的建模与分析中,我们不可避免的会遇到时间、空间性质描述的需求,但是,Alloy中缺乏了时间、空间概念的定义,这使得我们无法使用Alloy进行时空相关系统的建模与分析。因此,如何在Alloy的基础上构建出一个具有时空建模能力的语言显得尤为迫切。在时空性质的表示与推理中,空间逻辑提供了一组关系用来描述和判定对象之间是否存在某种空间上的联系;时态逻辑提供了一系列时态操作符来描述目标系统中时间相关的动作。本文通过对Alloy语言以及空间、时间逻辑的研究与分析,提出了一种时空建模与分析语言STALLOY,主要构建过程包括:1)基于Alloy语言以及空间、时态逻辑的特点,构造了符合Alloy语言规范的空间操作符和时态操作符,通过将它们作用到空间原子变量区域上,来产生用于时空推理与演算的空间变量集合;2)将区域演算理论与空间操作符结合,构建了一组空间关系用来表示空间区域或区域项之间是否存在某种空间上的联系,同时将时态操作符引入一阶布尔逻辑公式来描述时间相关的性质;3)对Alloy的一阶关系逻辑进行扩展,加入构造的时态、空间操作符和关系,构建了时空建模与分析语言STALLOY,并根据拓扑时空模型给出了它的语法和语义;4)经过分析,给出了STALLOY的时空逻辑的计算复杂度是EXPSPACE完全的证明,并应用它对时空系统中若干性质进行了描述。在构建了STALLOY语言后,我们给出了它的工具实现,其中包括:1)基于拓扑关系数据模型,我们将空间区域抽象为拓扑多边形,并据此给出了空间操作符的实现算法,同时结合Alloy语言给出了空间关系的实现;2)在构建了STALLOY时序关系的基础上,实现了时态操作符以及时态关系;3)将STALLOY时空逻辑的实现应用到Alloy开源工具中构造出了 STALLOY的工具。本文最后以列车防护系统为例,通过应用STALLOY及其工具对系统进行时空建模、分析和验证,展示了 STALLOY进行时空系统建模与分析的能力。
[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.
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP311.52

【参考文献】