胡指铭， 黄丽桃， 赵涌鑫

1. 华东师范大学软件工程学院， 上海 200062 2. 北京轩宇信息技术有限公司, 北京 100190

0 引 言

航天嵌入式软件及其运行环境具有高度的复杂性和不可预测性等特点，这就要求建模语言必须要有刻画系统和环境不同组件的表达能力，并且可以刻画面向嵌入式软件的模型特征，同时具有组合性和表达多重交互模式的能力.而周期控制系统语言SPARDL部分解决了前面的问题，但仅关注离散时间的动力系统，缺乏与物理世界的交互，为了实现对外部物理对象和环境的实时感知、可靠性信息传输、精确的动态控制与协调等目标，需要提出的语言能够对离散的控制逻辑和连续的物理变化建模，并描述它们之间的交互行为，从而更好地进行正确且精确的验证分析.

基于以上目的，本文提出了航天混成描述语言HSPARDL.为了更好地表示控制系统与物理世界的交互，在原有基础上引入了连续变量来描述物理设备组件的状态，并用微分方程来表示其变化规律，还引入了两个事件结构When和Until来连接物理设备和控制器.基于此框架，可以将物理过程和控制过程的描述和设计置于统一的形式化框架下，并且通过对该混成建模语言的形式化语义研究，消除由于自然语义二义性所引起的歧义性，揭示混成建模语言各语句的本质计算行为，从而为航天嵌入式系统的分析、设计、推理和验证提供坚实的理论基础.

1 航天混成描述语言HSPARDL

1.1 SPARDL

在介绍……