基于UPPAAL和UML的实时系统形式化分析与应用

计算机的应用模式在经历了主机模式和个人机模式后,目前正向最适合人类使用的普适计算模式发展。在普适计算模式下,实时系统将会渗透到人们生活的方方面面,为提高人们的生活质量发挥重要的作用。在这种情况下,实时系统的质量和开发效率往往会对一个产品的成功起着决定性的影响。为了保障实时系统的实时性、安全性和可靠性等,本文在深入研究了时间自动机、UPPAAL、UML的理论基础上,采用时间自动机与UML相结合的建模方法,使用UPPAAL对所建模型进行分析与验证,并结合两个实例说明了本方法。 采用形式化方法对实时系统进行分析和验证是提高其安全性、可靠性的一条重要途径。目前时间自动机是用于实时系统建模的重要形式化工具,它刻画了实时系统与时间有关的行为特征,反映了实时系统控制行为的可视转向。UML顺序图着重体现对象间动态的交互关系,而且具有良好的易理解性。但是UML顺序图用来对实时系统建模和验证还存在时间描述方面的不足,因此本文研究了利用UML的扩展机制对UML顺序图进行扩展的方法,扩展后的UML顺序图不但能够很好地保持原来的易理解性,而且能够精确地描述实时系统的时间需求。使用扩展后UML顺序图对实时系统建模,结合UML顺序图与时间自动机的形式化语义,将顺序图转化为时间自动机,然后采用模型检测工具UPPAAL对其进行形式化的分析与验证,最后结合咖啡机控制系统与交通灯控制系统实例,进一步说明本文所给方法在实时系统中的应用。