基于模型的实时系统形式化验证方法研究与实现-冯博洋.docx

《基于模型的实时系统形式化验证方法研究与实现-冯博洋.docx》由会员分享，可在线阅读，更多相关《基于模型的实时系统形式化验证方法研究与实现-冯博洋.docx（84页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

1、 硕 士 学 位 论 文 题 目： 基于模型的实时系统形式化验证方法 _ 研究与实现 _ 研宄生 ： _ 冯博洋 _ 专 业 ： _ 计算机技术 _ 指导教师 ： _ 方景龙教授 _ 完成日期 _ 2016年 3月 杭州电子科技大学硕士学位论文 基于模型的实时系统形式化验证方法 研究与实现 研 究 生 ： 冯 博 洋 指 导 教 师 ： 方 景 龙 研 究 员 2016年 3月 Dissertation Submitted to Hangzhou Dianzi University for the Degree of Master Research and implemention of mo

2、del based real-time system formalization validation Candidate: Boyang Feng Supervisor: Prof. Jinglong Fang March, 2016 杭州电子科技大学 学位论文原创性声明和使用授权说明 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研 宄工作所取得的成果。除文中已经注明引用的内容外，本论文不含任何其他个人 或集体已经发表或撰写过的作品或成果。对本文的研宄做出重要贡献的个人和集 体，均已在文中以明确方式标明。 申请学位论文与资料若有不实之处，本人承担一切相关责任。

3、论文作者签名： 日期： 年月 日 学位论文使用授权说明 本人完全了解杭州电子科技大学关于保留和使用学位论文的规定，即：研宄 生在校攻读学位期间论文工作的知识产权单位属杭州电子科技大学。本人保证毕 业离校后，发表论文或使用论文工作成果时署名单位仍然为杭州电子科技大学。 学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全 部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。（保密论文 在解密后遵守此规定 ） 论文作者签名： 日期： 年 月 日 指导教师签名： 日期： 年 月 日 摘要 随着计算机技术的发展，尤其是实时系统在各个领域的渗透，软件工程领 域中对实时系统的功能

4、行为、资源利用状况、能量消耗等特性的认识越来越深入， 如何才能够在系统模型设计阶段保证其可靠性已经成为领域内关注的热点。在系 统开发的过程中， UML已经成为设计人员广泛使用的建模语言，尤其是计时图 拥有出色的时间因素表现能力是实时系统建模的不二选择。由于 UML是一种半 形式化的建模语言，不能直接在其基础上进行模型验证，而时间自动机模型是一 种完全形式化的语言， UPPAAL是基于时间自动机的验证工具，可以对实时系统 进行实时功能验证。因此本文以计时图模型作为实时系统的建模模型，通过模型 转换算法将其转换为 UPPAAL中的时间自动机验证模型。 本文首先介绍了实时系统形式化验证的相关理论与技

5、术，给出了 UML计时 图和时间自动机的形式化描述，改进现有的模型转换方法，将计时图模型转换为 时间自动机。然后利用转换后的时间自动机进行功能验证，并对时间自动机做了 进一步的扩展，给出了资源时间自动机、能耗时间自动机的形式化定义，在其基 础上进行资源、能耗的非功能验证。最后根据本文研宄的形式化验证方法，实现 了原型工具 T-RTSMD， 并在两个不同应用领域的实例上验证了该方法的有效性。 关键词： 计时图，时间自动机，实时系统，形式化，验证 ABSTRACT With the development of computer technology, especially the applica

6、tion of real-time system in various areas, the features, which include function behavior, the resource utilization and energy consumption of real-time system in the field of software engineering, are getting more and more in-depth understanding. How to ensure the reliability of a real-time system du

7、ring its model design phase becomes a focus of the field. During the process of system development, Unified Modeling Language (UML) has widely used by the designers. And it becomes the best choice for modeling the real-time system due to the excellent performance of the time diagram in time factor.

8、However, UML is a half-formalized language which cannot be used to achieve the model verification directly. On the other hand, the timed automata model is a fully-formalized language, which can be employed by UPPAAL to achieve the real-time functional verification. Therefore, in this thesis the mode

9、l of the real-time system is modeled by the timing diagram, and then transformed as the timed automata model in UPPAAL by the model transformation algorithm. In order to verify the real-time system, the formal verification method is proposed in this thesis, Firstly, we introduce the relevant theory

10、and technology of the real-time system, give the formalized description of UML timing diagram and timed automata, and transform the timing diagram model into timed automata by improving the existing model transformation method. Then the functional behavior and the non-functional behavior are verifie

11、d by the timed automata and its extension, respectively. In the extension, the formal definitions of resource and energy consumption timed automata are defined. According to the method mentioned above, the Real Time System Model Design (T-RTSMD) is implemented. In addition, the validity of the propo

12、sed method is verified by two examples of different application fields. Key words: Timing Diagram, Timed Automata, Real-time System, Formalization, Verification. 目录 摘要 . I ABSTRACT . II 第 一 章 绪 论 . 1 1.1研究背景及意义 . 1 1.2国内外的研究现状 . 2 1.3论文主要研究内容 . 4 1.4论文章节安排 . 4 第二章相关理论与技术 . 6 2.1实时系统概述 . 6 2.2 UML 模型

13、 . 7 2.3时间自动机 . 9 2.4 UPPAAL . 11 2.5小结 . 12 第三章 UML计时图到时间自动机的转换 . 14 3.1模型转换依据 . 14 3.2模型转换算法的改进 . 14 3.2.1 Lifeline 转换为 Template . 15 3.2.2 State 与 Duration Constraint 的转换 . 19 3.2.3 Event 转换为 Guard. 26 3.2.4 Timeline 转换为 Clock . 30 3.2.5 Message 转换为 Channel . 30 3.3模型整体转换算法 . 33 3.4小结 . 34 第四章实时系

14、统的形式化验证方法 . 35 4.1实时系统形式化验证的相关定义 . 35 4.1.1消息场景约束 . 35 4.1.2状态空间的可达图 . 35 4.1.3投影路径 . 36 4.2实时系统的功能验证 . 37 4.2.1存在 一 致性验证 . 37 4.2.2前向 一 致性验证 . 38 4.2.3逆向 一 致性验证 . 39 _ 杭州电子科技大学硕士学位论文 _ 4.2.4双向 1致性验证 . 40 4.3实时系统的非功能验证 . 41 4.3.1实时系统的资源验证 . 41 4.3.2实时系统的能耗验证 . 46 4.4小结 . 48 第五章 T-RTSMD验证工具的实现与应用 . 4

15、9 5.1原型工具 T-RTSMD简介 . 49 5.2 T-RTSMD系统结构设计 . 49 5.2.1前端处理模块的设计与实现 . 50 5.2.2功能验证模块的设计与实现 . 51 5.2.3 非功能验证模块 . 53 5.3 T-RTSMD 的应用 . 57 5.3.1饮料销售控制系统的实例验证 . 57 5.3.2橙子筛选控制系统的实例验证 . 63 5.4小结 . 68 第六章总结与臟 . 69 6.1总结 . 69 6.2未来的研究工作 . 70 致谢 . 71 参考文献 . 72 附录 . 76 第 一 章 绪 论 1.1研究背景及意义 随着智能设备的迅速普及，实时系统在整个社

16、会发挥着越来越重要的作用， 据分析统计，其广泛应用于智能制造、工业控制、交通运输 等 1与 人们生活息息 相关的领域，另外因其独特的实时特性，在军事防御、核能研宄、航空航天等多 个领域也存在广泛的应用。随着实时系统所扮演角色的不断丰富，其自身的规模 也在不断扩大，并且其软、硬件构成的复杂性也在与日俱增，由此导致整个系统 失效的概率也在逐年增 高 2。 实时系统是一种在运行时与外界进行信息交互的各种行为具备时间约束特 征的计算机系统。从广义上讲，实时系统属于一种应激式反应系统，其除了具备 一般计算机系统常见的功能性约束外，还必须满足高实时响应、高可靠性约束要 求。实时系统工作时，必须绝对满足其特

17、定的性能要求，错过一次微小的时间期 限约束就有可能带来灾难性后 果 3。 历史上，由于实时系统失效造成的事故屡见 不鲜。如， 1996年 6月 4日，欧洲航空航天局斥巨资制造的 Ariane 5型运载火 箭，因为惯性制导系统中的一个软件缺陷使得火箭在首次发射点火 37秒后就发 生爆炸，这枚研制周期长达十一年的火箭连同四颗卫星瞬间化为乌有，直接造成 近四百亿法郎的经济损失，更严重的是，还使该项目延期三年。 以上事件足以证明实时系统失效将带来巨大的损失。因此，近年来，人们对 实时控制系统的性能要求在不断提高，如何保证实时系统的高可靠性和安全性是 当今社会的一个焦点问 题 4。 故而，在进行复杂程度

18、更高的实时系统开发中，验 证实时系统是否满足相关的性能需求也是一个非常有价值的课题。可以说实时系 统规模与复杂度的迅速增长给计算机科学研宄领域带来了许多新的问题和挑战， 成为近几年来人们研宄的热点。 传统上，实时系统的设计、实现以及维护等工作是由相关领域的工程专家来 负责，并非计算机科学研宄人员关注的主要对象。以前，通常由于系统规模较小、 问题领域专一以及硬件资源的限制 等 5， 使得在软件工程领域中许多重要的技术 和方法或者无法在实时系统领域得到广泛应用，或者有意无意的被忽视。但是， 随着现代实时系统的内部结构变得越来越复杂，其相关功能实现以及安全性保证 也变得更急复杂。当今工业界和学术界有

19、已经认识到，仅仅依靠相关领域工程专 家的传统经验很难完成现在功能更加丰富、性能要求更高的实时系统开发。而随 着现代软件工程相关技术研宄的不断深入 ，涌现出了很多经典开发方法，如模型 驱动开发、领域驱动开发以及结构化开发等等。我们可以在复杂实时软件开发中 结合主流设计开发方法来解决面临的实际问题。 随着面向对象软件的迅速发展，模型设计在整个软件开发中占据着越来越重 要的位置，其不但是后续开发测试工作顺序进行的基础，更是整个软件满足需求 功能的保障。此外，模型设计阶段的工作将直接决定着软件开发的投入与成本。 据统计，开发中如果模型设计阶段出现某个错误没有得到修正，那么在开发后期 再进行修复时造成的

20、开发成本将增加 5-100倍 6。 因此，基于软件设计模型进行 实时系统验证在实际开发中很有价值。其最大的益处就是尽可能早的发现软件中 存在的缺陷，将大大减少软件失效的情况发生。 总之，依据软件的设计模型对使用广泛的实时系统进行验证，能够对整个 软件开发和测试工作的顺利进行起到很大的推动作 用 7， 能使实时系统的开发测 试资源得到更合理的安排，有利于实时系统更好的服务社会，服务大众。因此， 开展基于模型的实时系统验证相关研宄是很有必要，也是非常有价值的。 1.2国内外的研究现状 随着实时系统验证工作的不断推进，国内外出现了几十种实时系统模型方法 和验证工具，这些理论分布于数以百计的文献中，对

21、整个实时系统验证相关研宄 起到了巨大的推动作用。目前，国内外出现了一些比较有影响，并且非常实用的 模型检验工具，如 SPIN、 UPPAAL、 CHIC、 TICC、 Ptolemy II、 Timed COSPAN、 KRONOS 等。 最早的实时系统相关验证工作是由德国学者 C.A.Petri在 1962年开展了，通 过利用 Petri网技术对实时系统进行建 模 8， 然后依据 Petri网时序变迀特性再结 合自动及相关理论进行实时系统验证。 1992年 Alur R和 Dill D等人提出可以运 用 AADL描述语 言9来 实现实时系 统验证，他们提出将 AADL模型转换到一种 等价形式结构的模型，然后利用已有的模型验证方法来进行实时系统的验证。 面向对象建模的标准语言，在有关基于模型进行实时系统一致性验证的相关 研宄中，很多都是基于 UML模型开展的。基于 UML进行实时系统的相关研宄 分析在整个工作中占据着十分重要的地位 。 1994年由 Uppsala大学和丹麦 Aalborg 大学联合开发的 UPPAAL工具，在传统时间自动机基础上，通过自定义函数扩 充，能够实现对实时系统进行建模和验证，这也是现在运用最为广泛的一种实时 系统建模和验证工具。