基于UML与PVS的严格建模技术研究----嵌入式实时系统的严格建模-计算机软件与理论专业论文.docx

摘 要 在许多关键 复杂软件开发的分析 设计阶段对软件模型进行精确化验证有利于确保 系统的正确性 降低系统开发的费用 缩短开发周期 大部分嵌入式实时系统都是关键复 杂系统 在设计阶段对其模型的验证尤其重要 如何给嵌入式实时系统的开发人员提供界 面友好 易于使用 又能对设计模型进行精确化验证的工具一直是软件工程研究中的难点 软件设计的工具分为两类 工业界的面向对象方法 如 UML 具有直观 易用 与程序 设计语言密切相关等优点 已被大多数软件开发人员接受 然而 由于缺少精确定义的语 义 面向对象模型难以用于精确化验证 另一类方法是形式化方法 它们基于严格的数学 理论 使用形式化规范对系统建模 并且通过工具完成验证 然而 这类方法对使用者要 求较高 并且通常仅限于某一专用领域 大多数软件开发人员难以直接使用 PVS 是一种形 式化方法 提供基于高阶逻辑的规范语言以及集成了模型验证(Model Checking) 定律证 明(Theorem Proving)的工具支持 现有许多研究都试图通过结合 UML 与形式化方法的优点 提供一种易于使用的 并且 根据需求提供相应程度形式化验证的软件方法 这些方法一般先使用 UML 对系统进行建模 然后将 UML 图形转换成相应的形式化规范语言 并使用相应工具进行验证 现有的研究中 大部分都是对静态属性的验证 在动态属性方面的研究比较少 同时 静态属性往往是动 态属性的基础 对某个模块独立地进行动态属性验证并不完整 在这一方面 使用 UML 与 形式化方法结合来提供解决方案的研究还很少 针对以上问题 本文提出了一种新的方法用于嵌入式实时系统的严格建模 这种方法通 过构造面向对象语言 UML 以及形式化方法 PVS 之间的转换桥梁 为一个嵌入式实时系统的 开发团队提供了一个易用 可以实现模型阶段验证的软件方法 该方法将为一个开发团队 提供工具的支持 该团队包括 UML 建模人员以及形式化验证人员 UML 建模人员首先使用一 种带有扩展的 UML 子集对系统建立图形表示的最初模型 然后使用转换工具自动实现图形 到 PVS 可验证规范的转换 形式化验证人员得到 PVS 规范后对设计中的需求进行验证 并 且根据验证的结果修改原有的设计 最终达到严格建模的要求 本文的内容包括设计从 UML 类图以及带有时间扩展的状态图转换得到可以验证的 PVS 规 范语言表示的模型 具体分为两部分 第一部分建立了从 UML 类图转换到 PVS 规范的框架 利用 UML 的四层架构定义 首先对最基础的元元模型层进行形式化 将其使用 PVS 规范语 言表示 使用 PVS 规范定义最基本的类型 以及该类型的语义 在这个基础上 对元模型 进行形式化 并且在 PVS 规范语言表示的形式化元元模型的上下文中表示形式化的元模型 最后 在这个上下文中对任意用户定义的类图进行转换 得到 PVS 规范 该转换方法实现 了语法一致性的检查 确保了类图中的核心语义在 PVS 规范语言中得以表示 第二部分包括对嵌入式实时系统的动态模型的 UML 建模 模型的形式化 以及使用 PVS 验证 1 抓住嵌入式实时系统动态属性的两个主要特点 实时性 反应式 提出通过使用 带有时间扩展的 UML 状态图 可以比较完整地对一个嵌入式实时系统的动态行为进行建模 2 接着给出了精确的数学模型 时间化自动机(Timed Automata) 并设计从带时间扩展的 UML 状态图到时间化自动机的转换算法 实现了精确化建模 3 使用 PVS 的模型验证工具 实现时间化自动机模型的验证 提出了一种通过时钟约束空间划分的方法实现了将时间化 自动机的状态空间有限化的算法 并且在这个有限模型的基础上 使用 CTL 表示实时逻辑 TCTL 得出使用 PVS 规范语言表示的一个模型验证问题 本文的主要贡献包括两点 1对 UML 类图到 PVS 规范的转换上提出了基于元模型架构 的改进方法 2提出了一套完整的使用 UML 状态图以及 PVS 实现嵌入式实时系统动态模型 的严格建模方法 并且实现了实时特性的建模与验证 关键词: UML PVS 时间化自动机 模型验证 Abstract Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development. Most of embedded real-time software are complex and critical systems. Tools supporting modeling and verification