随着计算机科学与技术的快速发展,实时系统的应用范围越来越广,其规模也越来越大,如何在系统设计阶段保障实时系统的可靠性逐渐成为近几年的研究热点。在实时系统的设计阶段,通常会对实时系统建立UML时序图模型,这样可以为后续的系统开发提供可视化指导。为了保证所建模型正确,满足系统的可靠性要求,需要对模型进行验证。由于UML模型是一种半形式化的模型,缺少精确的语义,因此直接对其进行验证比较困难,而时间自动机模型作为一种形式化模型能够在一些实时系统验证工具中很方便地对其进行验证,其中UPPAAL是基于时间自动机理论的形式化验证工具,它广泛应用在通信协议分析、列车系统运行等很多实时性系统的验证方面,但是时间自动机模型往往难以阅读和理解,所以其难以作为后续开发的可视化指导。为了便于设计开发人员利用正确的UML时序图进行后续开发,从而保证实时系统的可靠性,本文首先分析了 UML时序图和时间自动机中模型元素的相关语义,研究了现有的从UML时序图到时间自动机的转换算法,在其基础上针对实际应用中存在的问题进行了改进,提出了改进后的转换算法,将UML时序图转换为时间自动机。其次由于转换后的时间自动机缺乏布局,在验证时还需要人工拖拽以完成布局,为了自动化地完成布局以便于在UPPAAL中对时间自动机进行验证,本文基于现有的有向图布局算法,针对时间自动机中存在的回路问题,提出了改进后的时间自动机布局算法,对转换后的时间自动机自动进行布局。最后在对时间自动机进行验证后,如果发现错误,则直接在UPPAAL中对时间自动机进行修正,得到正确的时间自动机,为了设计开发人员能够使用正确的UML时序图作为可视化指导进行后续开发,基于对UML时序图和时间自动机模型元素的语义分析,本文提出了一种从时间自动机到UML时序图的转换算法,利用该算法将正确的时间自动机转换为UML时序图。基于以上的转换算法和布局算法,本文设计并实现了面向实时系统的模型转换与布局工具MT&L,并结合典型的实时系统实例对工具进行了相关说明。通过本文提出的方法在具体实例中的应用,可以看到该方法在满足实时系统高可靠性要求的同时,能够简化系统设计开发人员的工作,提高系统的开发效率。