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