中文摘要：

网络环境中，以组装服务构件的方式生成面向服务的软件系统是目前主流的软件开发范型。然而，现有的构件组装没有将构件的计算模型和协同模型分开讨论，组装方式是静态的，灵活性不够。服务构件协同建模是实现网络环境中服务构件动态组装所面临的主要问题之一，本课题旨在建模、规约和验证服务构件之间的协同行为，实现服务构件安全、灵活的组装，为提高软件系统的质量提供一种新的研究思路。研究基于Linda元组空间的服务构件安全协同模型，在元组总线上设置安全访问控制层，实现元组空间上安全、可靠的访问。研究基于该模型的服务构件协同规约语言，根据系统的安全需求，定义支持安全访问、动态组合的操作原语；研究协同规约语言的操作语义和指称语义模型，并基于程序统一理论（UTP）讨论语义模型之间的等价性。研究基于安全属性的组合验证算法，提高验证服务构件协同行为正确性的效率，并实现相应的原型系统。

结论摘要：

以组合服务构件的方式设计、开发可信的软件系统，能够有效提高软件开发的效率和质量，为面向服务的软件系统的设计、开发提供了一种有效的解决方案，具有重要的科学意义和应用价值。但是，其面临的主要问题是如何建模、验证服务构件的协同交互行为。针对该问题，本项目旨在研究如何建模、验证服务构件的协同行为，为设计、开发安全、可靠的软件系统提供一种可行的、有效的解决方案。主要的研究内容包括研究基于实时系统建模语言MARTE建模服务构件的协同行为；研究使用模型检测技术验证、分析服务构件的协同行为；结合轨道交通控制系统以及能量感知的智能建筑案例的分析和开发，进一步证实我们提出的解决方案的有效性、可行性。本项目的研究成果具有重要的科学意义，并为后续的研究工作打下了坚实的基础。