形式规范的自动验证算法的研究

发布时间：2018-03-01 19:08

本文关键词： MARTE 离散时间自动机接口自动机 Z语言模型检测　出处：《南京航空航天大学》2012年硕士论文　论文类型：学位论文

【摘要】：形式化方式包括了形式规范和设计验证两个方面，它的目的是以数学的方式来对系统进行描述，，为保证软件的可靠性提供条件。在现代软件系统开发过程当中，经常会要求在某些限定的时间约束之下，对系统的输入数据进行相应的处理，以及系统内部所进行的状态之间的变迁，最后给出对应的输出数据。本文的主要工作如下：本文首先介绍了一种结合接口自动机（Interface Automata）和Z语言的规范ZIA以及ZIAs之间的精化关系。然后研究了MARTE（Modeling and Analysis of Real-Time andEmbedded Systems），它在UML的基础上对于时间以及其他方面进行了一定的扩充。MARTE定义了基于模型的实时和嵌入式系统描述的基础。本文详细描述了MARTE中的一些基本和核心概念。然后给出了一种基于离散时间的ZIA模型规范（DT-ZIA），它不仅能够描述某些实时系统中针对在离散时间下的时间约束的要求，同时能够对系统的数据处理和状态变迁进行精确的表达。接着是MARTE的六元组表示，再接着是MARTE到DT-ZIA的转换方法。最后我们给出了在有限定义域上的ZIAs精化检测算法（包括算法的数据结构和流程图）、面向带有数据约束的实时系统的时序逻辑和在有限定义域上的DT-ZIA模型检测算法（包括实现类图和流程图）以及两个算法的实例验证。
[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.
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：TP334.7;TP301.1

【共引文献】