引言
　　随着微电子通信等技术的发展 嵌 入 式 系 统越来越多地应用 在 工 业 控 制汽 车航 空 航 天 等 任务关键和实时领 域 系 统 规 模 复杂度和性能需求不断 提 升 结构分析与设计语言的提出使嵌入式系统开发的重点从代码级提升到模型级 并可以对模型的各种功能属性和非功能属性进行分析 随 着 规范及附件内容 的 不 断 扩 展围绕其进行的 模 型 验 证 工 作 也 成 为 热 点 在 系 统开发早期的模型建立阶段就对模型的可调度性 安全性等方面进 行 验 证 可以避免设计过程的反复大大提高开发的效率 基于时间自动机理论 采用形式化方法通过过程模拟对模型的可调度性进行前期的验证是一种可行的方法
　　本文在研究 模型和时间自动机模型的基础上重点 讨 论 了 模 型 到 时 间 自 动 机 的转换针对 的执行模型和 附 件 模 型 分 别 给出了转换的方法 并 在 工 具 中 进 行 可 调度性的验证最后通过一个例子证实了转换和验证方法的可行性
　　背景知识
　　简介语言 是 年由美国汽车工程师协会 体 系 结 构 描述语言附属委员 会 嵌 入 式 计 算 系 统 委 员 会航 空电子系统公司共同提出的一种应用于嵌入式系统领域的体系结构建模语言 是设计和分析安全关键的嵌入式 实 时 系 统 的 软硬件体系结构的建模语言的组 件 包 括 软 件 类 执 行 平 台 类 和 系统类 三 大 类其 中 软 件 类 包 含 数 据 子 程 序线 程线程组进程五类组件执行平台类包含处理器 存储器设备总线四类组件系统类的系统组件是作为软件类组件和执行平台类组件的集成组件而设计的 除了这些组件及其连接关系描述的系统静态体系结 构 外 的 执 行 模 型 分 为 同 步和异步两种则是用来描述系统的运行时环境 用来管理和支持组件的执行 包括组件分发同步异步 通 信调 度模 式 变 换 等 行 为 线 程 和 子 程 序 组件是最小 的 执 行 和 调 度 单 元 线程可分为周期线程非周期线程 和 零 星 线 程 三 类它们的分派策略和对外部事件的响应各不相同行为模型 是对 标准语言所 构建模型的 进 一 步 精 化 是 以 的 行 为 附 件为基础描述 标准组件内部详细行为的模型 行为附件通过状态及状态变迁来描述行为变迁可以定义触发条件及变迁过程中发生的动作 条件和动作主要包括接收 发送数据子程序调用异步访 问执 行 时 间延 迟 时 间 等 且 通 过 层 次 并 发状态来支持更复杂的行为描述扩展的时间自动机理论在实时系统中某一种计算过程常常需要满足一定的时 间 约 束 为 此 提出了一种能够有效描述实 时 系 统 行 为 的 计 算 模 型 时 间 自 动机 时间自 动 机 是 在 有 限 自 动 机 的 基 础 上 添加了时间约束从而可以处理实时系统 时间自动机通过使用有限个真值时钟变量提供了一个简单而全面的方法来表示有时间约束的状态转换图 时间自动机的所有时钟在系统开始时从 开始计时并以同样的速率增加 每一次状态的转换都有可能复位一些时钟 通常使用标有事件标记的状态转换图对系统进行建模时间自动机的形式化定义和语义如下所示定义 时 间 约 束 设 为 时钟的有限集时钟限制的 集 合 按 以 下 语 法 定义给 定一个时钟集合 和一个时钟赋值一个时钟重置函数 是这样一种时钟赋值如果否则给定一个时 钟 赋 值 和 时 间 对 每 一 个我们定义定义 时 间 自 动 机 一 个 时 间 自 动 机 是 一个七元组 其中是外部符号的有限集 由两个集 合 组 成其中 是触发符号的集合 而 是被处触发符号的集合是内部符号的有限集合是控 制 状 态 的 有 限集合表示起始状态是时钟的有限集是一个函 数它 给 每 一 个 状态 赋 予 一 个 时 钟 限 制 被 称 作 不 变 条 件计算机工程与科学定义 时 间 自 动 机 的 语 义 一 个 时 间 自 动机的格局是一个有序对 包括控制状 态和在 上的时钟赋值 时 间 自 动 机 的 标 记 转换 系 统 如 下 表示简介的第一个版 本 于 年 发 行随后 一 直 由 大 学 和 大 学 联 合 开发和维护 它可用于时间自动机的建模 模拟和验证 中使 用 的 是 时 间 自 动 机 模 型并 且对时间自动机进行了一些扩展 可以声明一般值变量全局时钟和用于同步的通道 它在位置和通道上都对时间自动机进行了改进 采 用 的模型验证机制可以避免状态空间爆炸问题已被广泛应用于算法分析和协议验证方面 的主要优点是其运作的高效性和使用的方便性到时间自动机的转换为 了 对 建 立 的 模型进行形式化的验证我们需要 将 模型转换到时间自动机模型再用过 程 模 拟 的 方 法 对 状 态 的 可 达 性 进 行 判断从而对模型的可调度性进行验证 关键的问题在于如何将建立好的 模型 映 射 到 时 间 自 动机 模 型 且 保 证 语 义 的 一 致 性 以 下 分 别 对执行模型附件模型的转换过程做一阐述并给出转 换 到 工 具 可 识 别 模 型 的 一 般方法执行模型到时间自动机的转换在所建立 起 的 模 型 中系 统 的 调 度 执行不仅依赖于组件和组件之间的联系同时还依赖于模型设 定 的 运 行 环 境 在 标 准 中设 定系统同步或异步运行方式 支持组件运行和管理的虚拟运行环境被定义为执行模型在模型 转 换 过 程 中 我 们 主 要 关 注 的 是 系 统的调度方 式 和 数 据 的 流 动与 其 相 关 的 是中的线程组件处理器组件和端口关联在线程组件 中 包 含 两 个 与 调 度 相 关 的 属 性分别是分 派 策 略 ＿ 和 周 期其中 ＿ 的 属 性 值 包 含周 期 非 周 期 零 星 及后台四种 对应于这些分派策 略 需要设计不同的自动机模板 将调度的过程对应于时间自动机的状 态 转 移 中 去 所 设 计 模 板 包 含 的 主要状态应包括起始状态等待状态执行状态和错误状态以周期分派调度策略为例 形成的时间自动机模板如图 所示 其中 和是两个时钟变量 分别表示执行时间和截止时间 为线程设定的周期截止 时 间 对 应 于 模 板 中 的 属性 为线程执行的时间 两个时钟变量 和 时间属性 之 间 的 关 系 是 时 间 自 动 机 状 态 转 移的使能条件 为 一 组 触 发 状 态 迁 移 的 同 步信号对应于线程组件中的输入事件端口 当 该 端口从外部输入事件时 分 派 被 触 发 此 外还 需 要设计一个自动机用于产生周期的触发信号两个自动机之间 形 成 时 间 自 动 机 网 络通 过 通 道传递触发的信号 另一种触发迁移的信号 是允许执行的 条 件 它 是 来 自 于 处 理 器 组 件 的 调 度 信息 和 也 是 时 间 自 动 机 网 络 定 义 中 的通道在截止时间 前如果线程没有执 行 完 成 负责错误判断的自动机便会发送 信 号该 自 动机接收到 后转 移 到 错 误状 态当 满 足 完白 海 洋 等基于时间自动机的嵌入式软件模型可调度性验证成条件收到 信 号该 自 动 机 转 移 到等待派发状态非周期零星和后台三种调度策略可 类 似 地转换成不同模板的自动机 只是所形成的状态要略微复杂 它们的触发分派事件来自外部 且是随机的需要设计更多的时间自动机来负责分派事件的触发图 周期分派调度策略转换成的时间自动机模板处 理 器 组 件 是 能 调 度 和 执 行 线 程 的 执 行 平 台组件它 包 含 的 ＿ 属 性 用 于 设置调度策略有两个可选值 和是 指 最 早 截 止时间优先算法任 务 的 截 止 时 间 越 近 其 优 先 级 越高 是指单调速率调度算法该 算 法 用 于 周 期 任 务 的 调 度任 务 周期越短优先级越高进程组件根据自己的调度策略 选择调度绑定在其上的线程组件 这种调度可以转换成时间自动机中使能条件的设定规则 当满足一定的条件后负责调度的自动机通过通道向被调度的线程发送允许执行信号对应于图 中的端口组件分为数据端口 事件端口和事件数据端口可以用来传递数据或事件消息数 据 的 依 赖 关 系 和 传 递 事 件 的 先 后 顺 序 是 影响模型可调度性的关键因素 并且在线程的调度中也涉及端口的关联关系 所以端口组件和端口关联也是模型转换 工 作 的 关 键 相关的转换工作主要是根 据 输 入 及 输 出 的 关 联 关 系 来 进 行 的 将模型中 系 统 组 件 线程组件单独转换成一个自动机模板每个端口作为一个单独的状态根据数据产生的速率 要求到达的时间和数据传递关系等来设 置 自 动 机 的 约 束 状 态 转 移 的 使 能 条 件跨系统的端口数据传递可以用时间自动机网络中的通道或者全局时钟来转换例如在 模型中的端口描述转换成的时间自动机模型如图 所示图 端口组件到时间自动机转换实例行为模型到时间自动机的转换的行为附件 是 基 于 自 动 状 态 机 的 转 换理论提出的 行为附件的文法定义 包 含 六 个 可选块如下所示＿？？？？？＿行为模型描 述 了 组 件 内 部 的 详 细 行 为模式并与其他组件通过端口连接形成的流进行交互 每个组件内的行为模型是相互独立的转换成一个时间自动机 多个组件交互的行为转换成时间自动机间的交互 形成时间自动机网络 具体的转换方法如下行 为 附 件 中 状 态 迁 移 的 使 能 条 件和迁 移 过 程 动 作 分 别 对 应 于 时 间自动机的迁移使能条件 和迁移过程发生的动作行 为 附 件 中 的 分 为 三 类 条 件条件和端口事件 条 件 和 条 件 表示在布尔型条件下发生状态迁移与时间自动机模型下的状态迁 移 使 能 条 件 一 致 而 端 口 事 件 表 示当组件的 某 端 口 接 收 到 输 入 事 件 时 状 态 发 生 迁计算机工程与科学移映射为时间自动机网络中的通道 行为附件中块描述的端口动作也表示组件通过端口输出时间或者变量的值 也可以映射为时间自动机网络中的通道行 为 附 件 在 块 中定 义 变 量 在 块 中 对 变 量 初 始 化转换成时间自动 机 中 的 时 钟通 道并 可 以 设 置 初始状态在初始 状 态 到 第 二 个 状 态 迁 移 时 执 行 赋值动作行为 附 件 中 块 声 明 动 机 的状态可以直接映射到时间 自 动 机 的 状 态行为附件中 块表示状态的迁移 对 应于时间自动机 中 的 位 置 迁 移 行 为 附 件 中的初始状态对应时间自动机中的初始位置在 行为附件中用于表示层次化的状态机而设定的行为模型的组合状态在时间自动机模型中无法表示成层次化的状态机只能将组合状态进行展平即将行为模型中的子状态机映射为时间自动机模 型 中 新 的 自 动 机 行 为 模 型中 块 描 述 组 件 之 间 的 连 接 和 交 互 的关系 在映射 时关联的组件映射为一个自动机再将连接映射为自动机网络中的同步通道＿ 块是行为模型 中 组 合 状 态的详细描述在 进 行 展 平 操 作 后 一般映射为新的自动机 但 是当存在多个子状态并发运行的时候为实现转换 后 的 并 发 操 作可以将组合状态映射为触发每个子自动机运行的通道从时间自动机模型到 模型的转换为 了 使 用 工具对时间自动机模型进行可调度性的 验 证 还 需 要 按 照 的 规范将时间自动机模型做一些调整在时间 自 动 机 模 型 中 时间在状态迁移过程中流 逝而 在 中时间在状态上流逝状态转移认为是瞬间完成的 为了完成转换可以在 中增加中间位 置 对 应 于 自 动 机 的 状态 时间的流逝通过一个可达的状态来表示在 时 间 自 动 机 的 基 础 上 引 入 了一些 新 的 特 性 如 模 板常 量有 界 整 型 变 量 广 播通道紧 急 通 道紧 迫 位 置约 束 位 置 等 这 些 特 性可以使自动机的模型得到大量的简化 转 换 过 程中应当注意 中 不 支 持 实 型 变 量 原 模 型中的实型数值只能对应到整型数值转换中要本着严格约束的原则 以免在实际的调度中产生错误实际的转换工作是通 过 平 台 下 开 发 的转换 器 实 现 的 输 入 通 过 工 具 建 立 的模 型 文 件 该 文 件 后 缀 名 为 符 合标准 通过 解 析 模 型 文 件 获 得 模 型 的 基 本组件和属性并取得行为附件 执行转换规则生成时间自动机的基 本 模 型 再 输 出 为 可 识别的 文件建模转换与验证实例实 例 首 先 在 工具中建立一个嵌入式系统模型将 模 型 的 文件通过模型转换器转换成 对 应 的 时 间 自 动 机 模 型 输 出 为 格式在 中 打 开 模 型 文 件 进 行 模 拟 和 验证工作 过程如图 所示图 模 型 建 立转换和验证过程模型的建立建立一个 数 据 采 集 器 的 模 型其 功 能为通过采集器采集数据 通过输出端口发送给控制器的输入端口控制器中有一个进程组件负 责 对数据进行加密加密后的数据发送给监视器进行显示 模型如图 所示图 数据采集器系统 模 型 图选取 系 统 组 件 为 例 进 行 说 明 其代码为白 海 洋 等基于时间自动机的嵌入式软件模型可调度性验证模型转换转 换 后 的 模 型 生 成 了 中 的 三 个 模板 ＿ ＿ ＿和 ＿ ＿ 对 应 于 模 型中的 系 统 组 件 和 进 程 组 件并声 明 了 全 局 变 量 和 模 型每 个 模 板中也声明了所需的变量图 模拟过程中各模板状态迁移情况模型验证用 打开时间自动机模型 仍 以为例得到如图 所示的模板整个系统模拟的状态迁移如图 所 示 每 个矩形框表示一个状态 垂直的粗线表明当前状态转移的情况 表示不同模板间的消息流＿ ＿图 ＿ ＿ 模 板 图在 验证器 中 输 入 验 证 语 句 可 以 验证系统的可调度性 例 如验 证性质不满足说明系统存在死锁 因 为 在 监 视 器 获得输入后 没 有 状 态 的 转 移所 以 验 证 结 果 是 正 确的 验证 ＿ ＿＿ ＿ ＿＿ 性 质 可 满 足 说明计算线程必定在控制器输出端口输出前完成计算并返回结 果 并且时钟周期值小于 满 足 系 统设计需要
　　结束语
　　本文介绍了嵌入式软件建模语言 及 模型验证的相关理论 基于形 式 化 方 法 将 模型转换到 时 间 自 动 机 模 型并 利 用 模 型 验 证 工 具计算机工程与科学进行系统可调度性的验证 重点给 出 了执行模 型附件模型到时间自动机转换的一般方法 最后给出了验证的实例 展示了从建模到模型转换到模型验证的全过程鉴于 的 标 准 尚 不 完 善 的 语 义规则可能不能满足转换所需的全部条件所以目前的转换方法还需人工调整 转换的正确率也有待提高
　　参考文献＿＿附中文参考文献郭 华 庄 雷 张 习 勇 一种适合自动验证实时 系 统 的 工 具 微 计 算 机 信 息作者简介白 海 洋 男江 苏 徐 州 人 硕士 生研究方向为软件可靠性李 静 女吉 林 伊 通 人 博 士副 教 授 研究方向为图像处理赵 娜 女辽 宁 彰 武 人 硕 士生研 究 方 向 为 物 联 网白 海 洋 等基于时间自动机的嵌入式软件模型可调度性验证