摘要：基于接口自动机(Interface Automata,简称IA)的原理,提出了基于IA的Web服务组合设计方法,每一个Web服务对应一个IA模型,并使用IA的组合表示服务组合,当用户需求发生变化时,可以重新构建IA和组合IA,当需求稳定后,通过查找IA组合使用的路径就可以找到Web组合的方法,使用本文的方法可以快速生成满足用户需求的新应用系统。

摘要：针对构件式系统中任一构件的非良构性会导致系统不能正常运行的问题,提出一种基于接口自动机(IA)来分析和检测构件良构性(well-formedness)的算法,并据此实现了一个构件良构性检测原型系统。该算法首先构造与接口自动机同构的可达图;其次,基于可达图通过深度优先遍历生成一条覆盖所有迁移的有序集;最后,根据该有序集检测在外界环境满足其输入假设的情况下,每个属于方法的活动到其对应返回活动的路径的自治无异常可达性,从而实现接口自动机的良构性检测。根据所提算法在Eclipse平台设计并实现了构件良构性检测原型系统T-CWFC,该系统通过JFLAP建立构件的接口自动机模型并构造其可达图,进而对接口自动机作良构性检测并输出相关检测信息。最后通过对一组构件的良构性检测实验验证了算法的有效性。

摘要：Web应用的快速发展及其一些异于传统程序的特点使Web应用的验证面临了新的挑战。使用接口自动机对Web应用的构件和构件组合进行行为建模,设计了接口自动机到模型检验器Spin程序的转换算法,然后利用Spin检验Web应用的性质,通过一个简单的网上银行示例说明了整个验证过程。

摘要：在已有的研究基础上、基于接口自动机理论提出了一种构件交互形式化方法模型。它将接口自动机的输入输出动作分别对应为构件接口所提供的调用接口和使用接口,以接口自动机的组合来描述构件间的交互。在此构件模型基础上,提出了为不匹配的构件自动产生构件适配器的构件适配算法。

摘要：针对复杂业务流程设计测试效率低、自动化程度不高、测试用例正确性难以保证的问题,在研究接口自动机模型的基础上,提出了一种基于模型的业务流程测试方法。该方法首先采用扩展带约束的接口自动机对业务流程设计进行形式化描述,并给出了从业务流程设计模型到带约束的接口自动机模型的转换算法;然后基于模型完成了对业务流程设计与需求的一致性验证,将验证后的接口自动机模型作为业务流程的测试模型,通过其特有的"乐观方法"和博弈思想实现了流程间的嵌套调用组合;最后定义了业务流程的测试覆盖准则,并在满足活动约束条件组合覆盖准则的前提下,设计了相应的测试用例生成算法。实例分析表明:该方法能够简化测试过程,可用于业务流程设计的测试用例自动化生成,有效保证了测试用例的正确性,提高了测试效率。

摘要：使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.

摘要：在复杂的实时软件系统中使用构件式设计方法,已成为目前软件工程中的研究热点.如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一.通过在接口自动机模型中添加时间区间标记,来扩展其对实时系统接口行为的表达能力;使用实时接口自动机网络来描述实时软件系统的构件式设计模型;使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约,对系统设计阶段实时软件构件的动态行为进行形式化分析与检验.通过对实时接口自动机网络状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了验证算法,以检验构件式实时软件系统的设计与带时间约束的场景式规约之间的一致性.

摘要：从嵌入式软件设计模型层对构件化实时嵌入式软件系统中能耗相关性质进行研究,包括:扩展了实时接口自动机在能耗语义方面的描述能力,通过引入状态能量消耗率,建立了能耗接口自动机形式化模型以及自动机网络,用以建模嵌入式软件设计阶段系统构件及其构件组合的能耗行为特征;对能耗接口自动机网络的状态空间进行了形式化分析,构造了相应的可兼容整型空间的可达图,并在此基础上给出了最小能耗计算和最大能耗验证的算法。

摘要：基于设计模型的分析技术是现代复杂嵌入式软件系统高可靠性的重要保障手段。基于即时验证(On-the-flyverification)方法对一个构件化嵌入式软件设计模型原型验证工具T-CBESD进行了改进设计与实现。集成Topcased和JFLAP扩展了T-CBESD图形化建模接口;设计并实现了相关输入处理与转换;重新设计并实现了状态空间数据结构,包括功能、非功能行为(实时、资源、能耗等)验证问题在内的多个基于路径的一致性即时验证算法。给出了改进工具在火灾预警系统中的应用实例与分析。

摘要：现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.