计算机应用 | 古代文学 | 市场营销 | 生命科学 | 交通物流 | 财务管理 | 历史学 | 毕业 | 哲学 | 政治 | 财税 | 经济 | 金融 | 审计 | 法学 | 护理学 | 国际经济与贸易
计算机软件 | 新闻传播 | 电子商务 | 土木工程 | 临床医学 | 旅游管理 | 建筑学 | 文学 | 化学 | 数学 | 物理 | 地理 | 理工 | 生命 | 文化 | 企业管理 | 电子信息工程
计算机网络 | 语言文学 | 信息安全 | 工程力学 | 工商管理 | 经济管理 | 计算机 | 机电 | 材料 | 医学 | 药学 | 会计 | 硕士 | 法律 | MBA
现当代文学 | 英美文学 | 通讯工程 | 网络工程 | 行政管理 | 公共管理 | 自动化 | 艺术 | 音乐 | 舞蹈 | 美术 | 本科 | 教育 | 英语 |

初探一种构件化嵌入式软件设计模型验证工具

2013-07-03 01:06
导读:电子信息工程论文毕业论文,初探一种构件化嵌入式软件设计模型验证工具论文模板,格式要求,科教论文网免费提供指导材料:   1. 引言   嵌入式计算系统已经广泛

  1. 引言

  嵌入式计算系统已经广泛的应用于生活中的各个领域,如:交通、能源、医疗、控制、通信、军事等。近年来随着计算机硬件性能的不断提高,嵌入式系统中软件的规模和复杂性不断增加,使软件对整个系统的影响逐渐占据了统治地位。关键系统中的嵌入式软件失效将会导致生命与财产的重大损失。因此,嵌入式软件通常具有极高的功能可靠性、严格的实时性等要求,如何保证系统同时满足给定的功能和非功能需求已成为当前高可信嵌入式计算领域中的研究热点。目前,工业界已有一些比较有效的嵌入式软件测试和调试方法(如:在处理器中嵌入ICE 功能,调试代理软件,JTAG 模拟等)。但从软件工程的角度来看,这些方法都是在系统的开发中后期阶段所使用,而在嵌入式软件设计与分析的前期阶段还缺乏有效的方法和工具对系统设计进行分析与验证。
  本文基于接口自动机模型对构件化嵌入式软件设计(CBESD: Component-BasedEmbedded Software Designs)的分析与验证方法展开进一步研究,在Eclipse 开放平台上实现了一个CBESD的模型分析与验证原型工具T-CBESD(a Tool for Component-based EmbeddedSoftware Designs)。该工具的目的是应用于构件化嵌入式软件开发的设计建模阶段,对设计者所关心的系统重要功能性质以及与时间相关的实时行为性质进行严格形式化分析和验证,提高系统可靠性的可信度。
  本文内容安排如下:第2 节中给出了非实时功能行为验证以及实时功能行为验证的理论基础,包括:描述系统动态行为的多种接口自动机模型,基于场景的系统规约描述模型,以及形式化分析与验证的抽象算法等。在第3 节中给出了原型工具T-CBESD 的基本设计思想,非实时功能行为验证模块以及实时功能行为验证模块的设计与实现,包括:工具输入输出接口设计、状态空间数据结构设计、基于场景的系统规约模型的输入预处理、具体验证算法的设计与实现等。第4 节中给出了应用实例研究;最后是相关工作比较和结束语,对本文中原型工具的特点、意义以及进一步的工作进行简要讨论。

(科教范文网http://fw.ΝsΕΑc.com编辑)
  2. 工具的理论基础

  软件工程中的构件化设计方法学通过复用和组合软件模块来构造系统,从而提高系统开发效率和可靠性。通常,一个复杂的嵌入式系统由多个计算子系统构成,其软件系统也具有较高的构件化特征,因此,构件化的设计已成为解决嵌入式软件设计复杂性问题的一种手段。与此同时,构件接口之间的交互场景也成为体现系统行为复杂性的一个重要方面。
  本文中所讨论的原型工具就是使用形式化的接口自动机模型来对系统构件接口动态行为进行设计建模,并使用UML 交互概观图模型来描述多种基于场景的构件交互行为规约,然后应用形式化分析算法对设计模型是否满足系统规约进行分析和验证。

  2.1 建模系统构件以及组合行为
  接口自动机(interface automata,简称IA)是用来刻画软件构件接口交互行为时序特征的一种形式化语言。它描述了一个构件被使用的时候其对外界环境的输入假设和输出保证,即构件内方法被调用的先后次序以及构件对外环境输出调用信息或结果的次序。
  输入动作可以用来建模:1)构件内可以被调用的方法或过程;2)通信信道的接收端;3)调用外部过程的返回等。输出动作可以用来建模:1)对其他构件中的方法或过程的调用;2)通信信道的发送消息端;3)构件中方法或过程的调用结束时的返回;4)构件中方法或过程执行中出现的异常返回,等。内部动作则表达了两个构件在组合过程中的同步交互行为。
  考虑到嵌入式软件的实时性建模需求,需要对IA 进行实时语义的扩展,以增强接口自动机对实时系统的描述能力。直观上,对接口自动机每一个转换添加时间区间约束,以表示此转换发生的最小、最大时限;扩展后的模型称为实时接口自动机。

(转载自http://www.NSEAC.com中国科教评价网)

  我们使用接口自动机的组合状态空间来表达多构件系统的组合行为;自动机组合状态空间中每一条可能的状态转换序列用来表达多构件系统的一个组合行为轨迹。基本IA 和扩展的RTIA 组合状态空间的定义略有不同,以下只给出了RTIA 组合空间(实时接口自动机网络)的定义;不带时间语义的基本接口自动机的组合定义参见文献。

  2.2 基于场景的交互行为规约

上一篇:不同数量高斯光束通过相位屏的计算机仿真试验 下一篇:没有了