中文摘要：

针对具有模拟和数字构件、并且在开放和分布计算环境中，构件交互通过不同通讯设备和机制的异构嵌入式系统，本项目将致力于其建模、控制器设计和验证等的多学科研究。主要内容包括(1) 使用和扩展rCOS从而支持异构嵌入式系统的多层和多维的结构模型。其中此点又包括a) 在rCOS中引进物理构件并用差分和微分方程定义其不同模式行为。b) 研究构件间的依赖关系并定义组合算子。c) 定义语言使其具有连续构件以及连续和数字构件的异构连接器和协调器；d) 构件的不同视点。e) 语义定义使其能表达离散和连续行为的结合及物理构件的模式切换。(2) 利用不同的语言（逻辑）描述系统和个体构件不同视点模型的需求和性质。(3) 混合构件的设计模型。包括混合控制的形式规范、局部控制器的设计以及混合控制的形式设计。(4) 定义和分析构件的不同视点如何影响整体系统的需求和行为。(5) 具体工业实例的研究。

结论摘要：

针对异构嵌入式系统,主要对需求描述和分析、模型的实时和可信性理论、模型检验算法以及实例分析等方面进行了研究。并发表高质量理论论文5篇,目前培养博士2名和硕士6名。项目主要研究结果有 1. 零配置协议的形式建模和验证。利用模型检验和所定义的新的抽象关系进行零配置协议的形式建模和验证。我们的模型显示了RFC的一些错误。对此协议任意数目的主机和IP地址，我们提供了互斥特性的两种证明方法(1)手工操作证明,(2)利用模型检验以及所定义的新的抽象关系进行证明。 2.扩展的线性时段演算（ELDI）的有界模型检验. 对于不含有独立变量和量词的近似语义下的时段演算模型检验，Franzle和Hansen通过将该问题规约成为Presburger算术问题，获得一种4维指数时间复杂度下的模型检验算法。对于相同的时段演算子集在标准离散语义下的有界模型检验问题，在我们以前工作的基础上，将此问题规约成时间自动机的可达性问题来求解，所需的时间复杂度为公式大小规模的单指数以及模型状态个数的平方级别。 3.ELDI模型检验工具的软件实现 工具运用C++实现，并与UPPAAL相结合来检验给定的时间自动机A是否满足某个EDLI性质Φ。 4. 从面向对象模型到基于构件模型的互动转换。我们讨论了如何使面向对象设计模型自动地转化为一种构件模型，同时展示了一类将面向对象模型转化为构件模型工具的设计和实现方法，这些方法已在基于组件软件模型驱动设计的rCOS方法中被正式定义。利用QVT关系我们设计了这类转化，并将其实现作为rCOS CASE工具的一部分。 5. 混成实时和嵌入式系统建模与分析状态图形式规范。研究提出了一种扩展的状态图—混成实时和嵌入式系统建模与分析状态图，用于建立与分析混成实时和嵌入式系统模型。在混成自动机的基础上，对混成实时和嵌入式系统建模与分析状态图进行了改进,并定义其形式语法和语义。最后演示了列车控制系统的行为建模的实例。 6. 利用UML配置支持基于构件的形式开发我们给出使得形式化方法集成到实际的基于组件和模型驱动的开发的途径，该途径通过定义一个UML的配置文件来实现。我们着重于如何利用增量式和交互式的精化规则进行整个开发过程，在该工作中所采用的形式化方法是组件和对象系统的精化方法（rCOS），最后在CASE工具中利用一个例子来论证开发工作。