基于时间的 AADL 运行时服务形式化化

架构分析与设计语言（AADL）是用于设计制造由软件控制的机械系统的架构描述语言。AADL 标准（SAE International AS5506D）描述了要在按照标准定义的语义执行 AADL 模型时提供的运行时服务（RTS）。主要关注的是传输服务和计时服务。尽管文献[1]中提出的研究为 AADL 的形式语义奠定了基础，但未对时间建模。本文采用由 Kripke 结构定义的模态逻辑扩展并简化了这种形式化，以显式包含时间。AADL 标准中定义的 RTS 也扩展以支持行为规范附录标准语言（BA）的响应状态转换机器以及其 closely-related、形式化定义的对应项——嵌入式系统行为语言（BLESS）。本文还 presenting 了一种基于 High Assurance Modeling and Rapid Engineering for Embedded Systems（HAMR）实现的、用于 BLESS 中编写的状态转换机器行为的带时间的 AADL RTS 示例。