IF对实时软件设计图形模型的验证



IF对实时软件设计图形模型的验证

分类：教育论文网→工业技术论文→自动化技术、计算机技术论文→计算技术、计算机技术论文→计算机软件论文→程序设计、软件工程论文→软件工程论文

IF对实时软件设计图形模型的验证

论文目录
摘要	第1-4页
Abstract	第4-9页
第一章绪论	第9-12页
· 研究背景	第9-10页
· 研究内容及意义	第10-11页
· 本文的组织结构	第11-12页
第二章形式化方法与时间自动机理论	第12-18页
· 形式化方法	第12-14页
· 形式化描述	第12-13页
· 形式化验证	第13-14页
· 时间自动机	第14-17页
· ω-有穷自动机	第14-15页
· 时间语言	第15页
· 时钟约束和时钟解释	第15-16页
· 时间自动机的语法和语义	第16-17页
· 本章小结	第17-18页
第三章实时系统软件图形化设计模型	第18-32页
· 实时系统软件图形化设计模型介绍	第18-19页
· 实时系统软件图形化设计模型的对象和系统调用	第19-27页
· 任务	第19-21页
· 中断	第21-22页
· 警报	第22-23页
· 信号量	第23-24页
· 邮箱、消息、消息池	第24-25页
· 资源	第25-26页
· 事件	第26-27页
· 算法形式	第27-30页
· Forever	第27页
· If-Then	第27页
· While	第27-28页
· Repeat	第28页
· Switch and Case	第28-29页
· Procedure	第29-30页
· Insert command和Insert code	第30页
· 扩展	第30-31页
· 本章小结	第31-32页
第四章实时系统描述验证工具IF	第32-48页
· IF简介	第32-39页
· 体系结构	第32-34页
· IF表示	第34-36页
· IF的核心构件	第36-37页
· 静态分析	第37-38页
· 验证构件	第38-39页
· IF语义	第39-42页
· 抽象句法	第39-40页
· 操作句法:构型	第40-41页
· 操作句法:转移	第41-42页
· IF句法	第42-46页
· 结构	第42-43页
· 行为	第43-44页
· 数据	第44-46页
· 外部	第46页
· IF和其他形式化语言	第46-47页
· SDL	第46-47页
· LOTOS	第47页
· PROMELA	第47页
· 本章小结	第47-48页
第五章实时软件图形化设计模型到IF的映射	第48-59页
· 实时软件图形化设计模型的实时特征	第48页
· IF的实时特征	第48-49页
· 实时多任务模型到IF的映射方法	第49页
· 消息的映射规则	第49-50页
· 邮箱的映射规则	第50-51页
· 中断和报警的映射规则	第51页
· 信号量的映射规则	第51-52页
· 资源的映射规则	第52-53页
· 过程到IF的映射	第53页
· 算法形式到IF的映射	第53-54页
· 任务的映射规则	第54-57页
· 任务状态的映射	第55-56页
· 任务状态转换的映射	第56-57页
· 不匹配映射说明	第57-58页
· 本章小结	第58-59页
第六章实时软件图形化设计模型到IF映射的实现	第59-69页
· 需求描述	第59-60页
· 实时软件图形设计模型的建模	第60页
· 实时软件图形设计模型到IF的映射	第60-67页
· 主控任务的IF映射	第60-61页
· 信号获取任务的IF映射	第61-62页
· 监控任务的IF映射	第62-65页
· 整个煤气管道采集系统的IF映射	第65-67页
· 本章小结	第67-69页
第七章 IF对实时软件图形化设计模型映射的验证	第69-78页
· 静态分析	第69-73页
· 活变量分析	第69-72页
· 死代码清除	第72-73页
· 模型探测与生成LTS	第73-74页
· 模型验证	第74-77页
· 使用EVALUATOR验证	第74-75页
· 使用ALDEBARAN验证	第75-77页
· 本章小结	第77-78页
第八章总结和展望	第78-79页
致谢	第79-80页
参考文献	第80-86页
附录A 攻读学位期间发表论文	第86-87页
附录B 参与基金项目	第87 页

本篇论文共87页，点击这进入下载页面。

更多论文
IF对实时软件设计图形模型的验证
政府投资工程委托代建评标指标研究
基于RFID的制造执行系统及选择装配
女性不孕症患者焦虑抑郁影响因素研
价值工程在房地产项目规划设计中的
超（超）临界火电机组用钢数据库的
实时三平面组织多普勒技术对糖尿病
阿加曲班抗凝改性膜滤器的通透性能
双能量CTA对颅内动脉瘤的诊断价值研
基于网络的房地产项目远程管理研究
超声弹性应变率值在甲状腺良恶性结
超声弹性成像在乳腺病灶良恶性诊断
预应力锚索对洞室的加固机理试验研
长沙市区护士情绪劳动及其相关因素
框架—剪力墙结构的抗震分析和优化
长沙市护士卫生法律法规知识现状调
护士临床沟通能力量表的研制及应用
建设项目集成管理绩效评价理论与方
住房抵押贷款证券化的收益分析
基于支持向量机的工程项目投资风险
基于Windows平台活动目录域内软件资
中小房地产企业营销策略研究
一种基于模糊理论的网络学习评价系
3D网络游戏场景构件的研究和实现
磨损磨粒彩色铁谱图像的识别技术研
基于Web服务的工作流引擎的研究与实
肝脏磁敏感成像技术参数优选探讨及
领域术语自动抽取及关系分类研究
汽车线控制动之硬件系统研究
构件测试信息表示与检索的研究与实
64排螺旋计算机断层扫描在种植前颌
汽车排放测量技术与方法研究
基于Pro/E的部件BOM提取及产品BOM数
强脉冲光照射对体内外胶原蛋白合成
机动车颗粒物排放测试与研究
Galectin-1在高糖腹透液诱导人腹膜
基于DSP的运动目标检测系统研究
汽油品质对汽车排放及OBD系统影响的
高校信息安全服务外包风险的管理与
长沙地区县级医院中年慢性病患者的
车用质子交换膜燃料电池系统的气场
基于FPGA图像采集及JPEG压缩系统实
柴油车辆的排放及试验研究
时空关联成像技术在胎儿心脏检查中
对网格模型简化算法的研究和改良
液力变矩器三维流场仿真计算
医学图像三维重建算法研究及实现
汽车盘式制动器摩擦块偏磨机理的研
智能视觉监控中运动目标检测与跟踪
碳酸氢钠预防对比剂肾病的研究
新建本科院校教学质量保障体系研究
静脉铁剂不同给药方案对维持性血液
基于小波变换的图像分割技术
高职院校学生职业能力培养研究
前额皮质区与正负性情绪词执行加工
基于广义回归神经网络的图像测温方
制造业科技人才培养开发研究
基于视觉的多点触控系统关键技术研
高校教师科研评价研究
基于JDBC接口的嵌入式数据库在PDA上
基于公平与效率的高等教育财政拨款
基于运动目标跟踪的车流量统计技术
我国高等教育评估制度创新研究
视频图像序列中的人体运动分析
高等学校对其独立学院教学质量监控
调控巨噬细胞自噬对结核分支杆菌清
基于粒子滤波的运动目标跟踪算法研
我国公立高校筹资市场机制研究
基于视频的目标检测与跟踪的研究
我国硕士研究生培养模式研究
质谱法与直接测序法检测HBV P基因耐
基于GIDS的入侵检测集群技术研究
HJM利率期限结构模型与数值计算
FDC与板式组合药治疗肺结核的临床随
新型水阻试验系统的设计与实现
基于Web的企业竞争情报系统中权限构
低钠盐饮食对降压药物的疗效影响—
高校校园网论坛热点话题发现系统的
PW-DTI对高血压患者不同左室构型整
Web服务集成测试工具的设计与实现
基于众志863芯片的状态防火墙设计实
口令认证系统的安全性研究与实现
烟叶叶片结构在线检测系统的设计及
基于工作流的机车质量管理系统的设
基于Parzen窗估计与Renyi’s熵的动
辊压机粉磨系统的能耗模型及其工程
铝箔分卷监控系统研究与设计
珍珠岩大板液压成型机优化设计
基于人工神经网络的机器嗅觉系统研
装饰布企业车间生产调度的研究与应
内模控制算法在锅炉烟气脱硫pH值控
产品数据管理系统中工作流技术研究
人脐血干细胞静脉移植对急性心肌梗
面向Actor设计的无线传感器网络中机
替米沙坦对原发性高血压患者血清Ap
基于J2EE的港口企业信息门户的研究
自发性高血压大鼠花生四烯酸乙醇胺
地勤周期检管理信息系统的设计与实

实时系统论文时间自动机论文 IF 映射规则论文实时系统验证论文
版权申明：目录由用户张**提供，www.51papers.com仅收录目录，作者需要删除这篇论文目录请点击这里。
\| 设为首页\|\|加入收藏\|\|站内搜索引擎\|\|站点地图\|\|在线购卡\|
版权所有教育论文网 Copyright(C) All Rights Reserved