学位论文 > 优秀研究生学位论文题录展示

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

作　者: 沈嘉权
导　师: 刘晓燕
学　校: 昆明理工大学
专　业: 计算机应用技术
关键词: 实时系统时间自动机实时软件图形设计模型 IF 映射规则实时系统验证
分类号: TP311.52
类　型: 硕士论文
年　份: 2009年
下　载: 5次
引　用: 0次
阅　读: 论文下载

内容摘要

实时系统是能及时响应外部发生的随机事件,并以足够快的速度完成对事件处理的计算机应用系统。对于实时系统,不但要满足逻辑的正确性,而且要满足的时间的正确性,即对系统有时限要求,所要求的处理必须在一定的时限内完成,这就要求实时系统必须具有很高的可靠性,如果系统出现故障,将可能造成严重的后果。时间自动机是一种有效描述实时系统行为的计算模型,采用时间自动机对实时系统进行分析设计,可以有效地提高实时系统可靠性。时间自动机作为一种形式化方法,使用具有严格数学定义的语法和语义的规范语言来描述系统,但形式化方法不够直观,要掌握形式化描述方法也并不容易。而可视化的建模方法有着比较直观,易于理解的特点,广泛应用于软件的开发设计过程之中。但可视化建模本身缺乏精确语义,难以对建模模型进行分析和验证。若将可视化建模方法与形式化方法相结合,综合二者的优点,可以为实时软件建模提供良好的解决方案。本文将一个可视化实时软件图形设计模型工具与形式化描述及验证工具IF相结合,实现实时系统的建模、分析设计与验证的过程。本文首先介绍实时系统软件图形化设计模型的建模元素、建模思想和方法,然后对实时系统描述验证工具IF的体系结构、IF对实时系统的表示方式和方法、IF的语法和语义,以及运用IF工具集构件进行实时系统验证的方式和方法进行研究。通过分析和比较实时系统软件图形化设计模型和IF对所表示的实时特性,找出二者对应对象的相似之处,给出映射的规则和方法,并对不能映射部分进行了说明。最后通过一个实例实现实时系统软件图形化设计模型到IF的映射,把本文提出的映射规则运行用到实际应用中,再使用IF工具集对映射结果进行验证,检测对实时系统建模设计是否满足规定要求。

全文目录

摘要  3-4
Abstract  4-9
第一章绪论  9-12
  1.1 研究背景  9-10
  1.2 研究内容及意义  10-11
  1.3 本文的组织结构  11-12
第二章形式化方法与时间自动机理论  12-18
  2.1 形式化方法  12-14
    2.1.1 形式化描述  12-13
    2.1.2 形式化验证  13-14
  2.2 时间自动机  14-17
    2.2.1 ω-有穷自动机  14-15
    2.2.2 时间语言  15
    2.2.3 时钟约束和时钟解释  15-16
    2.2.4 时间自动机的语法和语义  16-17
  2.3 本章小结  17-18
第三章实时系统软件图形化设计模型  18-32
  3.1 实时系统软件图形化设计模型介绍  18-19
  3.2 实时系统软件图形化设计模型的对象和系统调用  19-27
    3.2.1 任务  19-21
    3.2.2 中断  21-22
    3.2.3 警报  22-23
    3.2.4 信号量  23-24
    3.2.5 邮箱、消息、消息池  24-25
    3.2.6 资源  25-26
    3.2.7 事件  26-27
  3.3 算法形式  27-30
    3.3.1 Forever  27
    3.3.2 If-Then  27
    3.3.3 While  27-28
    3.3.4 Repeat  28
    3.3.5 Switch and Case  28-29
    3.3.6 Procedure  29-30
    3.3.7 Insert command和Insert code  30
  3.4 扩展  30-31
  3.5 本章小结  31-32
第四章实时系统描述验证工具IF  32-48
  4.1 IF简介  32-39
    4.1.1 体系结构  32-34
    4.1.2 IF表示  34-36
    4.1.3 IF的核心构件  36-37
    4.1.4 静态分析  37-38
    4.1.5 验证构件  38-39
  4.2 IF语义  39-42
    4.2.1 抽象句法  39-40
    4.2.2 操作句法:构型  40-41
    4.2.3 操作句法:转移  41-42
  4.3 IF句法  42-46
    4.3.1 结构  42-43
    4.3.2 行为  43-44
    4.3.3 数据  44-46
    4.3.4 外部  46
  4.4 IF和其他形式化语言  46-47
    4.4.1 SDL  46-47
    4.4.2 LOTOS  47
    4.4.3 PROMELA  47
  4.5 本章小结  47-48
第五章实时软件图形化设计模型到IF的映射  48-59
  5.1 实时软件图形化设计模型的实时特征  48
  5.2 IF的实时特征  48-49
  5.3 实时多任务模型到IF的映射方法  49
  5.4 消息的映射规则  49-50
  5.5 邮箱的映射规则  50-51
  5.6 中断和报警的映射规则  51
  5.7 信号量的映射规则  51-52
  5.8 资源的映射规则  52-53
  5.9 过程到IF的映射  53
  5.10 算法形式到IF的映射  53-54
  5.11 任务的映射规则  54-57
    5.11.1 任务状态的映射  55-56
    5.11.2 任务状态转换的映射  56-57
  5.12 不匹配映射说明  57-58
  5.13 本章小结  58-59
第六章实时软件图形化设计模型到IF映射的实现  59-69
  6.1 需求描述  59-60
  6.2 实时软件图形设计模型的建模  60
  6.3 实时软件图形设计模型到IF的映射  60-67
    6.3.1 主控任务的IF映射  60-61
    6.3.2 信号获取任务的IF映射  61-62
    6.3.3 监控任务的IF映射  62-65
    6.3.4 整个煤气管道采集系统的IF映射  65-67
  6.4 本章小结  67-69
第七章 IF对实时软件图形化设计模型映射的验证  69-78
  7.1 静态分析  69-73
    7.1.1 活变量分析  69-72
    7.1.2 死代码清除  72-73
  7.2 模型探测与生成LTS  73-74
  7.3 模型验证  74-77
    7.3.1 使用EVALUATOR验证  74-75
    7.3.2 使用ALDEBARAN验证  75-77
  7.4 本章小结  77-78
第八章总结和展望  78-79
致谢  79-80
参考文献  80-86
附录A 攻读学位期间发表论文  86-87
附录B 参与基金项目  87

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

内容摘要

全文目录

相似论文