论文部分内容阅读
近年来,随着嵌入式系统结构的日益复杂化,传统手工式的嵌入式软件开发方法已经不能适应市场的需求。基于组件的软件工程方法在通用领域的大量成功应用使得人们开始将目光转向其在嵌入式系统构造中的应用。由于嵌入式系统实时性、资源有限性、多样性、高可靠性等领域特点,使得嵌入式软件系统的开发或多或少的引入了形式化的开发方法。但目前针对软件组件的形式化方法的研究主要集中于对原有方法进行扩充以实现对软件组件概念的描述,这使得软件组件的一些优秀特性不能够被充分的表达。
软件组件很难(或根本不可能)通过提供一组构造函数的代数方法来进行描述。它的形式语义实际上是基于观察的,也就是说它所有可见的动态行为都来自于它与外部环境的交互。因此,近来得到显著发展的共代数理论成为了对软件组件进行建模的较佳选择。
共代数理论的发展主要来自对代数与共代数对偶性的研究,而这种对偶性来自对范畴论中泛构造总是成对出现的基本观察。代数与共代数分别为静态(基于构造,面向数据)系统与动态(基于观察,面向行为)系统的建模提供了理论基础。从程序设计的角度看,初始规约与终结规约中数据与行为的对称性可以看作代数共代数对偶性的具体体现。
就目前的研究来看,利用共代数对软件组件及基于组件的软件系统建模主要集中于提供基础的形式语义,而对于嵌入式系统这样的具体领域还没有涉及。针对这一问题,本文主要进行了以下几方面的工作:
1、共代数的形式化基础-范畴论的研究与探讨。介绍了范畴论中的基本概念,并对泛性质与泛构造的关系进行了深入研究;
2、一般化软件组件共代数语义的研究。通过将组件规约分别对应F-共代数的基本结构,为软件组件提供了一个一般化的共代数模型;
3、嵌入式组件共代数模型的构造。通过对嵌入式系统的领域特性进行分析,提出了嵌入式软件组件模型必须满足的性质。通过实例化F-共代数的行为单子,使得组件行为具有确定性和无穷性。通过构造针对F-共代数载集的函数,实现了组件整体非功能属性的表达。通过构造三个集合范畴上的幺半群及其对应的强单子,实现了组件方法非功能属性的表达。提出了组件基于接口的显式依赖的概念;
4、基于嵌入式组件的软件系统模型的构造。通过三种基本方式实现了组件的聚合,并分析和验证了其对组件非功能属性的影响。通过分析聚合组件的性质,提出了标准输入输出接口的概念并定义了对应的输入输出转换结构。最后通过输入输出模拟基于依赖接口的组装,并通过实例分析了这种方法的优劣。