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

• 作者: 尤晋元 赖明志
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: 嵌入式系统 UML状态图 时间化自动机
• 年，卷（期）: 2003,（8）
• 所属期刊栏目: 研究与发展
• 页码范围: 4-6,14
• 页数: 4页
• 分类号: TP315
• 字数: 5111字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	尤晋元	上海交通大学计算机科学与工程系	99	1122	18.0	30.0
2	赖明志	上海交通大学计算机科学与工程系	4	69	3.0	4.0