电子发烧友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. 1XL4015+LM358恒压恒流电路图
  2. 0.38 MB   |  137次下载  |  1 积分
  3. 2PCB布线和布局电路设计规则
  4. 0.40 MB   |  4次下载  |  免费
  5. 3TPS6287B25降压转换器评估模块
  6. 3.46MB   |  1次下载  |  免费
  7. 4INA226EVM用户指南
  8. 4.7MB   |  1次下载  |  免费
  9. 5INA226EVM修订版A模型用户指南和软件教程
  10. 2.28MB   |  1次下载  |  免费
  11. 6Altium Designer印刷电路板设计与制作PDF电子书免费下载
  12. 14.11 MB   |  0次下载  |  3 积分
  13. 7DLPC3470和DLPC3478软件编程人员指南
  14. 1.68MB   |  次下载  |  免费
  15. 8TPS1213-Q1智能高侧驱动器评估模块
  16. 1.63MB   |  次下载  |  免费

本月

  1. 1XL4015+LM358恒压恒流电路图
  2. 0.38 MB   |  137次下载  |  1 积分
  3. 2新概念模拟电路第四册信号处理电路电子书免费下载
  4. 10.69 MB  |  60次下载  |  免费
  5. 3800VA纯正弦波逆变器的参考设计
  6. 2.96MB   |  34次下载  |  免费
  7. 4纯电动汽⻋的主要部件及⼯作原理
  8. 5.76 MB   |  15次下载  |  5 积分
  9. 5JESD79-5C_v1.30-2024 内存技术规范
  10. 2.71 MB   |  10次下载  |  免费
  11. 6elmo直线电机驱动调试细则
  12. 4.76 MB   |  9次下载  |  6 积分
  13. 7明伟电源模块RSP-3000图纸
  14. 0.30 MB   |  8次下载  |  免费
  15. 8使用BQ76PL102系列电量计进行BQ78PL114的快速入门指南
  16. 4.04MB   |  7次下载  |  免费

总榜

  1. 1matlab软件下载入口
  2. 未知  |  935115次下载  |  10 积分
  3. 2开源硬件-PMP21529.1-4 开关降压/升压双向直流/直流转换器 PCB layout 设计
  4. 1.48MB  |  420061次下载  |  10 积分
  5. 3Altium DXP2002下载入口
  6. 未知  |  233084次下载  |  10 积分
  7. 4电路仿真软件multisim 10.0免费下载
  8. 340992  |  191366次下载  |  10 积分
  9. 5十天学会AVR单片机与C语言视频教程 下载
  10. 158M  |  183329次下载  |  10 积分
  11. 6labview8.5下载
  12. 未知  |  81581次下载  |  10 积分
  13. 7Keil工具MDK-Arm免费下载
  14. 0.02 MB  |  73805次下载  |  10 积分
  15. 8LabVIEW 8.6下载
  16. 未知  |  65985次下载  |  10 积分