基于UML2.0顺序图的高可信实时软件建模技术研究

摘要

为了提高高可信实时软件开发的质量,研究了使用UML2.0顺序图建立高可信实时软件动态行为模型的方法.首先给出了顺序图在语法和语义上的形式化描述,分析了顺序图中事件之间的关系,在此基础上,给出了一种使用自动机描述每个对象在顺序图描述的场景中所参与的事件序列的方法,然后将该方法扩展到带有组合片段的UML2.0顺序图,最后分析了UML2.0顺序图中的时间建模机制,给出了从UML2.0顺序图中提取时间约束,从而将上一步得到的自动机转化为时间自动机的算法.以上工作为使用模型检测工具UPPAAL对顺序图进行进一步的分析与验证奠定了基础.