使用时间化自动机形式化带有时间扩展的UML状态图

摘要

严格建模是嵌入式实时系统设计的核心技术,通过UML方法与形式化方法结合可以给严格建模提供很好的工具支持.时间化自动机(Timed Automata)是一种用于描述、验证实时系统的理论模型.文中提出了一种通过时间化自动机来形式化带有时间扩展的UML状态图的方法,这种方法为UML与形式化方法的结合构造了桥梁作用.带有时间扩展的UML状态图用于嵌入式系统动态模型的建模,从时间化自动机模型得到形式化规范将更容易.UML状态图的形式化分为两部分完成:层次状态图的平面化以及时间化自动机的构造.