电子发烧友App

硬声App

0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示
电子发烧友网>电子资料下载>嵌入式开发>基于有限状态机的嵌入式系统模型校验技术

基于有限状态机的嵌入式系统模型校验技术

2017-10-27 | rar | 0.3 MB | 次下载 | 1积分

资料介绍

模型校验是最成功的需求验证工具。模型校验的基本原理如图1所示。模型校验工具的输入是系统需求或设计(称为模型)以及最终系统期望实现的特性(称为“规 范”)。如果给定的模型满足给定的规范,那么工具将输出yes,否则将生成反例。反例详细描述了模型无法满足规范的原因,通过研究反例,可以精确地定位模 型的缺陷,如此反复。该方法的原理是通过确保模型满足足够多的系统特性以增强我们对模型正确性的信心。系统需求之所以称为模型,因为这些模型表征的是需求 或设计。
  基于有限状态机的嵌入式系统模型校验技术
  图1:模型校验方法。
  那 么,哪种规范化语言可以用来定义模型呢?答案当然不是唯一的,因为不同应用领域的需求(或设计)差异很大。例如,银行系统和空间系统在系统规模、结构、复 杂度、系统数据的属性及执行操作上的需求差异就很明显。相反,大多数实时嵌入式或安全临界系统都面向控制,而不是数据,这意味着这些系统的动态特性远比业 务逻辑(由系统维护的内部数据的结构及操作)重要。这些基于控制的系统可以应用于诸多领域:航天系统、航空电子、汽车系统、生物医学仪器、工业自动化及过 程控制、铁路、核电站等。甚至数字硬件系统的通信和安全协议均可视为面向控制的系统。
  对于面向控制的系统,可以采用有限状态 机(FSM)定义需求和设计,这是一种得到广泛认可的抽象表示方法。当然,光靠FSM并不能对复杂的实际工业系统进行建模。我们还需要:1. 能将需求模块化并区分需求等级;2. 能合并各组成部分的需求(或设计);3. 能通过更新预先规定的变量和设备,防止可能出现的异常。
  校验设计需求时,通常可以通过回答一些问题得到结果。下面给出了校验需求时最常问的一些问题:
  * 设计需求是否准确地反映了用户需求?需求中的每一事项是否与用户的期望一致?需求是否包含用户所要求的全部内容?
  * 设计需求是否表述清晰并无异义?是否能被用户很好地理解?
  * 设计需求是否具有灵活性和可实现性?例如设计需求是否模块化并具有良好的架构,从而有助于设计和开发?
  * 设计需求是否能轻松地定义验收测试示例以验证设计实现与需求的一致性。
  * 设计需求是否只是概要地描述而与具体的设计、实现及技术平台等无关,从而使得设计人员和开发人员具有充分的自由度实现这些需求?
  回 答这些问题当然绝非轻而易举而且也没有任何捷径可循,但如果需求成功地超越了这些条条框框,那么无疑为优良系统的设计打下了坚实基础。尽管可以利用类似 UML这样的建模工具,但仍然需要确保设计需求的质量。这个过程需要投入大量精力和时间,包括各种形式的审查,有时甚至还需要进行部分原型设计。此外,需 求设计中采用多种表示方法(如UML中的表示方法)通常又将引发其他的问题,例如:
  * 设计需求需要使用哪种表示方法?
  * 如何确保不同表示方法的描述的一致性?
  基于有限状态机的嵌入式系统模型校验技术
  图2:简单的双水槽泵控系统。
  设计需求缺陷的成本通常很高,至少需要重设计并进行维护。错误的需求导致错误的系统行为并显著增加成本,如丧失产品的时效性和本质特征,而对于工作在实时环境下的嵌入式安全临界系统更是如此。为确保系统设计的质量,也需要考虑类似的问题。
  改 进需求和设计的一条途径是利用自动化工具对需求和设计各环节的质量进行校验。那么,哪种工具最适用呢?一般而言,校验用英文描述的需求或设计极为困难。因 此,必须采用一种清晰严格且无二义的规范化语言对需求进行描述。如果这种描述需求和设计的语言具有明确的语义,那么完全可以开发出自动化工具以分析这种语 言描述的设计需求。这种采用严格语言描述需求或设计的基本思想已成为系统验证的基石。
下载该资料的人也在下载 下载该资料的人还在阅读
更多 >

评论

查看更多

下载排行

本周

  1. 1TC358743XBG评估板参考手册
  2. 1.36 MB  |  330次下载  |  免费
  3. 2开关电源基础知识
  4. 5.73 MB  |  6次下载  |  免费
  5. 3100W短波放大电路图
  6. 0.05 MB  |  4次下载  |  3 积分
  7. 4嵌入式linux-聊天程序设计
  8. 0.60 MB  |  3次下载  |  免费
  9. 5基于FPGA的光纤通信系统的设计与实现
  10. 0.61 MB  |  2次下载  |  免费
  11. 6基于FPGA的C8051F单片机开发板设计
  12. 0.70 MB  |  2次下载  |  免费
  13. 751单片机窗帘控制器仿真程序
  14. 1.93 MB  |  2次下载  |  免费
  15. 8基于51单片机的RGB调色灯程序仿真
  16. 0.86 MB  |  2次下载  |  免费

本月

  1. 1OrCAD10.5下载OrCAD10.5中文版软件
  2. 0.00 MB  |  234315次下载  |  免费
  3. 2555集成电路应用800例(新编版)
  4. 0.00 MB  |  33564次下载  |  免费
  5. 3接口电路图大全
  6. 未知  |  30323次下载  |  免费
  7. 4开关电源设计实例指南
  8. 未知  |  21548次下载  |  免费
  9. 5电气工程师手册免费下载(新编第二版pdf电子书)
  10. 0.00 MB  |  15349次下载  |  免费
  11. 6数字电路基础pdf(下载)
  12. 未知  |  13750次下载  |  免费
  13. 7电子制作实例集锦 下载
  14. 未知  |  8113次下载  |  免费
  15. 8《LED驱动电路设计》 温德尔著
  16. 0.00 MB  |  6653次下载  |  免费

总榜

  1. 1matlab软件下载入口
  2. 未知  |  935054次下载  |  免费
  3. 2protel99se软件下载(可英文版转中文版)
  4. 78.1 MB  |  537796次下载  |  免费
  5. 3MATLAB 7.1 下载 (含软件介绍)
  6. 未知  |  420026次下载  |  免费
  7. 4OrCAD10.5下载OrCAD10.5中文版软件
  8. 0.00 MB  |  234315次下载  |  免费
  9. 5Altium DXP2002下载入口
  10. 未知  |  233046次下载  |  免费
  11. 6电路仿真软件multisim 10.0免费下载
  12. 340992  |  191185次下载  |  免费
  13. 7十天学会AVR单片机与C语言视频教程 下载
  14. 158M  |  183278次下载  |  免费
  15. 8proe5.0野火版下载(中文版免费下载)
  16. 未知  |  138040次下载  |  免费