中文摘要：

国际对象管理组织OMG将模型驱动架构，作为提高软件质量与开发效率最有前景的方法, 并于2010年8月发布模型驱动实时系统建模规范MARTE。但MARTE 模型缺乏严格的语义，特别是多时钟系统的时间关系语义，不能精确地描述带多类混合时间约束的模型系统，不能对反应性进行精确建模，并保证模型的正确性、一致性。本项目研究采用形式方法，探索解决多抽象层次、多视角MARTE模型中的时间关联、模型正确性验证、模型一致性几个关键问题的理论和方法。研究将统一程序理论与MARTE规范和时间约束语言CCSL结合起来，针对包含大量并发事件、随机事件的复杂实时系统软件设计中的关键问题，探索给出精确建模的方法，并给出模型转换规则、模型精化策略与有效进行模型验证的手段，最后将研究成果应用于上海轨道交通列控系统设计，力争为提高我国自主研发安全攸关实时系统软件开发能力作出贡献。

结论摘要：

项目的背景 模型驱动架构中，包含大量并发事件与随机事件的复杂实时系统模型构造、带时间约束的模型检查与模型一致性保证一直是系统可信性保证中的难题。国际对象管理组织 OMG发布了针对模型驱动式实时系统的建模规范 MARTE，但MARTE 模型缺乏严格的语义，特别是多时钟系统的时间关系语义，不能精确地描述带多类混合时间约束的模型系统，不能对反应性进行精确建模，并保证模型的正确性、一致性。本项目研究采用形式方法，探索解决多抽象层次、多视角MARTE 模型中的时间关联、模型正确性验证、模型一致性问题的理论和方法。主要研究内容 本项目主要研究实时系统软件建模规范 MARTE 和时间约束语言 CCSL，针对 MARTE 实时系统时间结构模型构造的特点, 建立统一的离散/稠密时间模型；研究 MARTE/CCSL 时间模型中的多时钟约束关联，和保证多视角、多抽象层次 MARTE 模型一致性策略；并对验证方法进行优化，验证安全性、活性；改进、扩充和完善本课题组已经开发的模型驱动可信软件开发系统Trustable MDA 1.0，以支持实时系统建模与验证。重要结果 本课题从建立MARTE规范统一的离散/稠密时间模型入手，将形式化的软件规约技术应用到MARTE多层次模型构建中，对实时系统软件类型的多样性、离散状态和连续状态统一性、软件实体和运行环境的协同等特性进行了深入的研究。建立了实时系统的状态模型、通信模型、构件模型、体系结构模型，并从语义上给出了模型的安全条件。系统地给出了一系列提高MARTE软件模型精确性和保持MARTE模型一致性的方法，以及面向轨道交通运控系统的优化验证策略。开发了模型驱动式可信实时系统软件集成开发环境。将研究成果与工具应用到北京房山线的列车控制系统。关键数据及其科学意义 在连续离散融合的混成系统模型研究中，我们获得了边迁移和一种特殊类型的演化迁移，边迁移发生在离散的时间点，而演化迁移则发生在两个离散时间点之间的时间区间。通过两类迁移可以同时对离散时间变量和连续时间变量的变化过程进行统一的描述。演化迁移可定义由模式中的连续变量的变化而引起的从模式到自身的迁移。在含有连续变量的系统中，当模式中的连续变量随着时间的流逝而变化时，通过该迁移可以将模式转变和系统环境联系起来。我们还获得了模型的安全语义和活性语义。