论文部分内容阅读
实时系统中任何一点错误都可能导致灾难性的后果,故保障实时系统的正确性和可靠性是建立实时系统的首要问题。实时系统建模无疑是一种很好的解决方法,但新的问题是如何保证实时系统模型的正确性和可靠性。这依赖于良好的建模语言和建模工具以及完善的仿真和验证工具。UML作为可视化描述软件结构和行为的标准语言,已经广泛应用在各种软件开发中,在实时系统领域也发挥了越来越重要的作用。目前对实时系统建模主要采用UML序列图(sequence diagram)与状态图(state diagram)相结合的方法。而UML时序图(Timing Diagram)不仅能描述对象间的状态转换同时还能完美地刻画交互次序和交互的时间细节。UML时序图强大灵活的描述能力使其在实时系统建模中必将发挥越来越重要的作用。实时系统的高可靠性要求必须对实时系统模型进行仿真和验证。UPPAAL是基于时间自动机的一个实时系统验证工具,具有强大的仿真和验证能力。但是UPPAAL只能验证UPPAAL时间自动机所描述的模型,不能对UML时序图模型进行仿真和验证。如果能将UML时序图模型转换为UPPAAL时间自动机模型,那么就可以利用UPPAAL对基于UML时序图的实时系统进行仿真和验证,且如果能够开发出转换工具实现自动转换,就可以使UML时序图模型直接作为UPPAAL的输入模型而不需要在UPPAAL中重新建立模型,从而缩短开发周期,降低出错概率。本文分析研究了UML时序图模型和UPPAAL时间自动机模型,提出了从UML时序图模型到UPPAAL时间自动机模型的转换策略。针对UML时序图各元素的语义以及UPPAAL时间自动机的相关语义,给出了将UML时序图模型映射到UPPAAL时间自动机模型的设计方案以及转换算法。同时,文章给出了基于上述UML时序图模型到UPPAAL时间自动机模型的转换规则和转换算法的工具UML_TDMtoUPPAAL_TAM。该工具能够按照已定义好的转换规则将UML时序图模型转换到UPPAAL的时间自动机模型,由UPPAAL对模型进行仿真和验证。UML时序图模型到UPPAAL时间自动机模型的转换使得UPPAAL能够对基于UML时序图模型的实时系统进行仿真和验证,使UML时序图模型直接作为UPPAAL的输入模型而不需要在UPPAAL中重新建立模型,从而缩短开发周期,降低出错概率,大大提高实时系统的可靠性。