基于UPPAAL和UML的实时系统形式化分析与应用-软件工程专业论文.docx

基于UPPAAL和UML的实时系统形式化分析与应用 中文摘要 基于UPPAAL和UML的实时系统 形式化分析与应用 中文摘要 计算机的应用模式在经历了主机模式和个人机模式后，目前正向最适合人类使用 的普适计算模式发展。在普适计算模式下，实时系统将会渗透到人们生活的方方面面， 为提高人们的生活质量发挥重要的作用。在这种情况下，实时系统的质量和开发效率 往往会对一个产品的成功起着决定性的影响。为了保障实时系统的实时性、安全性和 可靠性等，本文在深入研究了时间自动机、UPPAAL、UML的理论基础上，采用时 间自动机与UML相结合的建模方法，使用UPPAAL对所建模型进行分析与验证，并 结合两个实例说明了本方法。 采用形式化方法对实时系统进行分析和验证是提高其安全性、可靠性的一条重要 途径。目前时间自动机是用于实时系统建模的重要形式化工具，它刻画了实时系统与 时间有关的行为特征，反映了实时系统控制行为的可视转向。UML顺序图着重体现 对象间动态的交互关系，而且具有良好的易理解性。但是UML顺序图用来对实时系 统建模和验证还存在时间描述方面的不足，因此本文研究了利用UML的扩展机制对 UML顺序图进行扩展的方法，扩展后的UML顺序图不但能够很好地保持原来的易 理解性，而且能够精确地描述实时系统的时间需求。使用扩展后UML顺序图对实时 系统建模，结合UML顺序图与时间自动机的形式化语义，将顺序图转化为时间自动 机，然后采用模型检测工具UPPAAL对其进行形式化的分析与验证，最后结合咖啡 机控制系统与交通灯控制系统实例，迸一步说明本文所给方法在实时系统中的应用。 关键词：UPPAAI，；UML顺序图：实时系统：时间自动机：建模；模型检测 作‘ 者：赵丽芳 指导老师：张广泉  Abstract Analysis and Application ofReal-time Systems Based on UPPAAL and UML Formal Analysis and Application of Real—time Systems Based on UPPAAL and UML Abstract When the Pervasive Computing age is coming，the real-time system will be more and more important．Productivity and quality of the real-time system are crucial for success of the real—time system．In order to ensure real-time system’S safety and reliability，methods of analysis and verification of real-time systems that combines timed automata based on UPPAAL and UML are adopted in this paper． It is important to improve real-time systems’safety and reliability by adopting formal methods to carry on real-time systems analysis and designs．Timed automata is the main formal tools used in real-time systems’designs．Timed automata is an excellent graph-based notation for capturing timed control behaviour of systems．UML sequence diagram is highly intuitive and can clearly show the interaction among objects．However,it is not good at describing time requirement of real—time systems．In this paper we adopted a UML extended mechanism that not only can maintain UMLs intelligibility but also Call describe the time requirement of real-time system．We also adopted a method that Call translate UML