模型驱动架构中的可信嵌入式软件建模与分析

摘要	第1-7页
Abstract	第7-12页
第1章 绪论	第12-27页
·研究背景	第12-14页
·研究意义	第14页
·相关技术与研究现状	第14-23页
·软件体系结构与MDA	第14-15页
·UML	第15-16页
·UML MARTE Profile	第16-17页
·形式化模型与Petri网	第17-20页
·面向方面	第20页
·时态逻辑	第20-21页
·模型检测	第21页
·模型转换	第21-23页
·主要研究内容与研究成果	第23-25页
·课题来源	第23页
·主要研究内容	第23-24页
·主要研究成果	第24-25页
·论文结构	第25-26页
·本章小结	第26-27页
第2章 带MARTE标记的UML模型	第27-36页
·引言	第27-28页
·UML/MARTE建模方法	第28-30页
·MARTE Profile	第28页
·ACTIVITY/MARTE建模方法	第28-29页
·SEQUENCE/MARTE建模方法	第29-30页
·UML/MARTE模型的形式化定义	第30-35页
·ACTIVITY/MARTE的形式化定义	第31-33页
·SEQUENCE/MARTE的形式化定义	第33-35页
·本章小结	第35-36页
第3章 带抑制弧的时延着色PETRI网	第36-56页
·引言	第36-38页
·TCPNIA语法	第38-41页
·TCPNIA语义	第41-43页
·面向方面的TCPNIA	第43-45页
·TCPNIA的模型检测	第45-54页
·变迁冲突调解机制	第45-46页
·时间自动机与模型检测	第46-48页
·TCPNIA到时间自动机的转换算法	第48-52页
·TCPNIA到时间自动机的转换算法正确性	第52-54页
·TCPNIA到时间自动机的转换算法复杂度	第54页
·本章小结	第54-56页
第4章 基于TCPNIA的嵌入式系统调度	第56-65页
·引言	第56-57页
·TCPNIA的状态表示	第57页
·用TCPNIA建模实时嵌入式系统	第57-60页
·数据与控制建模	第57-58页
·模块化建模	第58-60页
·调度分析	第60-64页
·可调度性判断算法	第60-62页
·算法的正确性	第62-63页
·算法复杂度	第63页
·调度算法可组合性分析	第63-64页
·本章小结	第64-65页
第5章 UML模型图到TCPNIA的转换	第65-96页
·引言	第65-66页
·模型等价判断规则	第66-67页
·带MARTE标记的活动图到TCPNIA的转换	第67-86页
·动作节点映射规则	第67-69页
·对象节点映射规则	第69-72页
·控制节点映射规则	第72-82页
·流的映射规则	第82-84页
·组合方法	第84-86页
·带MARTE标记的序列图到TCPNIA的转换	第86-95页
·生命线映射规则	第87-90页
·消息映射规则	第90-92页
·事件映射规则	第92-94页
·组合方法	第94-95页
·本章小结	第95-96页
第6章 实例分析	第96-115页
·引言	第96页
·实例描述	第96-98页
·UML模型	第98-100页
·带MARTE标注的活动图模型	第98-99页
·带MARTE标注的序列图模型	第99-100页
·UML模型到TCPNIA模型的转换	第100-110页
·带MARTE标注的活动图到TCPNIA的转换	第100-108页
·带MARTE标注的序列图到TCPNIA的转换	第108-110页
·模型性质分析	第110-114页
·模型检测	第110-113页
·可调度性分析	第113-114页
·本章小结	第114-115页
第7章 总结与展望	第115-117页
·论文总结	第115-116页
·工作展望	第116-117页
参考文献	第117-128页
致谢	第128-129页
攻读博士学位期间发表的论文	第129-131页
攻读博士学位期间参加的科研项目	第131页