摘 要

接口自动机是一种形式化工具，用来描述基于组件系统中组件和组件之间的交互行为。通过接口自动机的并行组合操作，可以有效的描述软件构件之间的组装过程和结果。因此，本文重点研究接口自动机的组合算法的实现和分析。

本文以XML描述算法的输入文件格式，基于Myeclipse平台和Java语言实现系统开发，并且使用SWT设计界面来展现运行的结果。主要工作包括：首先介绍接口自动机组合算法研究的背景意义以及国内外的研究现状；其次对接口自动机组合算法的开发工具以及开发平台和相关知识进行描述，并说明组合算法中几个重要的数据结构的设计；最后，结合java语言以及相关技术来实现这个接口自动机的组合算法并且通过案例对组合算法的执行过程进行了分析说明。

关键词：接口自动机；自动机组合；组合算法；java

Analysis and Implementation of the Algorithms for Interface Automata Composition

ABSTRACT

Interface automaton is a formal tool that describes the interaction between components and components based on component systems. Through the parallel operation of the interface automaton, it can effectively describe the assembly process and the result between the software components. Therefore, this paper focuses on the realization and analysis of the combination algorithm of interface automata.
In this paper, XML describes the algorithm input file format, based on Myeclipse platform and Java language system development, and use the SWT design interface to show the results of the operation. The main work includes: Firstly, it introduces the background significance of the research on the algorithm of interface automata and the research status at home and abroad. Secondly, the development tools and development platform and related knowledge of interface automaton combination algorithm are described, and several important Finally, the combination of java language and related technology to achieve the interface automaton combination algorithm and through the case of the combination of the implementation of the algorithm described in the analysis.

Key words：interface automata；automata composition；combination algorithm；Java

目 录

第1章 绪论 1

1.1 论文研究背景和意义 1

1.2 国内外研究现状 1

1.3 论文研究内容和结构 2

第2章 开发工具简介 3

2.1 java以及SWT简介 3

2.2 开发工具JDK和平台MyEclipse简介 3

第3章 接口自动机组合算法 5

3.1 接口自动机的非形式描述 5

3.2 接口自动机的形式化描述 6

3.3 接口自动机的组合算法 6

3.4 本章小结 7

第4章 算法的数据结构设计 8

4.1 状态数据结构 8

4.2 转换关系数据结构 8

4.3 接口自动机数据结构 9

4.4 接口自动机XML文件存储结构 10

第5章 接口自动机组合工具的实现 14

5.1 读XML文件模块 14

5.2 接口自动机构造模块 14

5.3 接口自动机组合模块 16

5.4 界面设计 21

5.5 本章小结 23

第6章 案例分析 25

结论与展望 32

致 谢 33

参考文献 34

1. 绪论

1.1 论文研究背景和意义

随着信息技术的发展，我们越来越看重一个系统的可靠性，虽然我们不可能开发出一个完全正确或者百分之百安全的系统，但是我们可以通过形式化方法来大大提高系统的可靠性程度以及信心。形式化方法（Formal Methods）是软件工程中提高系统可靠性的一种重要方法，通过应用这种方法我们可以得到在不同抽象层次上描述整个或部分系统行为的规约和模型^[1]。

接口自动机是一种在构件化设计中用来建模软件构件接口时序特征行为的形式化语言^[2]。 并且接口自动机会有输入动作和输出动作以及内部的转换动作，其中内部动作描述的是在自动机内部由一个状态通过特定的动作（action）转换到下一个状态，输出动作可以用来建模，就是对方法的调用、调用终止以及方法执行的时候出现异常之类的。但由于一个构件化系统是通过多个构件子系统相互组合而成，这就涉及到接口自动机的组合问题，只有将多个接口自动机的模型组合起来，才能得到我们想要的完整的系统动态模型。所以，本毕业设计就是实现接口自动机的组合算法，为基于接口自动机的模型检验相关工作提供一个良好的基础，并且这也是模型检验工具中的一个基本模块。

1.2 国内外研究现状

近年来，基于构件的设计（Component-Based Design，CBD）技术的应用越来越被广泛的应用于大规模、复杂嵌入式软件开发，他带来的好处有便捷、可靠、灵活以及高效。组件的额粒度可大可小，小到一个过程，一个对象或一个模块，大到一个代理、一个服务或一个应用软件包均可看作是组件。组件仅通过接口来与环境进行交互，因此常采用对接口进行形式化描述的方法来刻画组件的特性。关于这方面的研究长期以来一直受到学术界和产业界的重视^[3]。

2001年由Luca de Alfaro和Thomas A.Henzinger正式提出一种新的用于描述接口的理论－－接口自动机（Interface　Automata）^[4]。与已有的各种方法都不同，在该理论中有两个突出的特点：“乐观方法”（optimistic　approach）和博弈（game）思想。前者用于定义开放式系统中的接口兼容问题。后者用于描述之一问题的语义。