资料介绍
模型校验是最成功的需求验证工具。模型校验的基本原理如图1所示。模型校验工具的输入是系统需求或设计(称为模型)以及最终系统期望实现的特性(称为“规 范”)。如果给定的模型满足给定的规范,那么工具将输出yes,否则将生成反例。反例详细描述了模型无法满足规范的原因,通过研究反例,可以精确地定位模 型的缺陷,如此反复。该方法的原理是通过确保模型满足足够多的系统特性以增强我们对模型正确性的信心。系统需求之所以称为模型,因为这些模型表征的是需求 或设计。
图1:模型校验方法。
那 么,哪种规范化语言可以用来定义模型呢?答案当然不是唯一的,因为不同应用领域的需求(或设计)差异很大。例如,银行系统和空间系统在系统规模、结构、复 杂度、系统数据的属性及执行操作上的需求差异就很明显。相反,大多数实时嵌入式或安全临界系统都面向控制,而不是数据,这意味着这些系统的动态特性远比业 务逻辑(由系统维护的内部数据的结构及操作)重要。这些基于控制的系统可以应用于诸多领域:航天系统、航空电子、汽车系统、生物医学仪器、工业自动化及过 程控制、铁路、核电站等。甚至数字硬件系统的通信和安全协议均可视为面向控制的系统。
对于面向控制的系统,可以采用有限状态 机(FSM)定义需求和设计,这是一种得到广泛认可的抽象表示方法。当然,光靠FSM并不能对复杂的实际工业系统进行建模。我们还需要:1. 能将需求模块化并区分需求等级;2. 能合并各组成部分的需求(或设计);3. 能通过更新预先规定的变量和设备,防止可能出现的异常。
校验设计需求时,通常可以通过回答一些问题得到结果。下面给出了校验需求时最常问的一些问题:
* 设计需求是否准确地反映了用户需求?需求中的每一事项是否与用户的期望一致?需求是否包含用户所要求的全部内容?
* 设计需求是否表述清晰并无异义?是否能被用户很好地理解?
* 设计需求是否具有灵活性和可实现性?例如设计需求是否模块化并具有良好的架构,从而有助于设计和开发?
* 设计需求是否能轻松地定义验收测试示例以验证设计实现与需求的一致性。
* 设计需求是否只是概要地描述而与具体的设计、实现及技术平台等无关,从而使得设计人员和开发人员具有充分的自由度实现这些需求?
回 答这些问题当然绝非轻而易举而且也没有任何捷径可循,但如果需求成功地超越了这些条条框框,那么无疑为优良系统的设计打下了坚实基础。尽管可以利用类似 UML这样的建模工具,但仍然需要确保设计需求的质量。这个过程需要投入大量精力和时间,包括各种形式的审查,有时甚至还需要进行部分原型设计。此外,需 求设计中采用多种表示方法(如UML中的表示方法)通常又将引发其他的问题,例如:
* 设计需求需要使用哪种表示方法?
* 如何确保不同表示方法的描述的一致性?
图2:简单的双水槽泵控系统。
设计需求缺陷的成本通常很高,至少需要重设计并进行维护。错误的需求导致错误的系统行为并显著增加成本,如丧失产品的时效性和本质特征,而对于工作在实时环境下的嵌入式安全临界系统更是如此。为确保系统设计的质量,也需要考虑类似的问题。
改 进需求和设计的一条途径是利用自动化工具对需求和设计各环节的质量进行校验。那么,哪种工具最适用呢?一般而言,校验用英文描述的需求或设计极为困难。因 此,必须采用一种清晰严格且无二义的规范化语言对需求进行描述。如果这种描述需求和设计的语言具有明确的语义,那么完全可以开发出自动化工具以分析这种语 言描述的设计需求。这种采用严格语言描述需求或设计的基本思想已成为系统验证的基石。
图1:模型校验方法。
那 么,哪种规范化语言可以用来定义模型呢?答案当然不是唯一的,因为不同应用领域的需求(或设计)差异很大。例如,银行系统和空间系统在系统规模、结构、复 杂度、系统数据的属性及执行操作上的需求差异就很明显。相反,大多数实时嵌入式或安全临界系统都面向控制,而不是数据,这意味着这些系统的动态特性远比业 务逻辑(由系统维护的内部数据的结构及操作)重要。这些基于控制的系统可以应用于诸多领域:航天系统、航空电子、汽车系统、生物医学仪器、工业自动化及过 程控制、铁路、核电站等。甚至数字硬件系统的通信和安全协议均可视为面向控制的系统。
对于面向控制的系统,可以采用有限状态 机(FSM)定义需求和设计,这是一种得到广泛认可的抽象表示方法。当然,光靠FSM并不能对复杂的实际工业系统进行建模。我们还需要:1. 能将需求模块化并区分需求等级;2. 能合并各组成部分的需求(或设计);3. 能通过更新预先规定的变量和设备,防止可能出现的异常。
校验设计需求时,通常可以通过回答一些问题得到结果。下面给出了校验需求时最常问的一些问题:
* 设计需求是否准确地反映了用户需求?需求中的每一事项是否与用户的期望一致?需求是否包含用户所要求的全部内容?
* 设计需求是否表述清晰并无异义?是否能被用户很好地理解?
* 设计需求是否具有灵活性和可实现性?例如设计需求是否模块化并具有良好的架构,从而有助于设计和开发?
* 设计需求是否能轻松地定义验收测试示例以验证设计实现与需求的一致性。
* 设计需求是否只是概要地描述而与具体的设计、实现及技术平台等无关,从而使得设计人员和开发人员具有充分的自由度实现这些需求?
回 答这些问题当然绝非轻而易举而且也没有任何捷径可循,但如果需求成功地超越了这些条条框框,那么无疑为优良系统的设计打下了坚实基础。尽管可以利用类似 UML这样的建模工具,但仍然需要确保设计需求的质量。这个过程需要投入大量精力和时间,包括各种形式的审查,有时甚至还需要进行部分原型设计。此外,需 求设计中采用多种表示方法(如UML中的表示方法)通常又将引发其他的问题,例如:
* 设计需求需要使用哪种表示方法?
* 如何确保不同表示方法的描述的一致性?
图2:简单的双水槽泵控系统。
设计需求缺陷的成本通常很高,至少需要重设计并进行维护。错误的需求导致错误的系统行为并显著增加成本,如丧失产品的时效性和本质特征,而对于工作在实时环境下的嵌入式安全临界系统更是如此。为确保系统设计的质量,也需要考虑类似的问题。
改 进需求和设计的一条途径是利用自动化工具对需求和设计各环节的质量进行校验。那么,哪种工具最适用呢?一般而言,校验用英文描述的需求或设计极为困难。因 此,必须采用一种清晰严格且无二义的规范化语言对需求进行描述。如果这种描述需求和设计的语言具有明确的语义,那么完全可以开发出自动化工具以分析这种语 言描述的设计需求。这种采用严格语言描述需求或设计的基本思想已成为系统验证的基石。
下载该资料的人也在下载
下载该资料的人还在阅读
更多 >
- 基于有限状态机的车身防盗报警的实现
- LSM6DSOX嵌入式有限状态机的使用和配置
- 如何以面向对象的思想设计有限状态机
- C语言状态机编程思想
- 有限状态机设计是HDL Designer Series的关键应用 6次下载
- 如何使用FPGA实现序列检测有限状态机 12次下载
- 有限状态机在嵌入式软件中的应用 27次下载
- VHDL有限状态机设计-ST 3次下载
- 有限状态机_FSM_的实现 0次下载
- 有限状态机FSM在PLD中的实现分析 3次下载
- 有限状态机在嵌入式系统中的实现及应用 1次下载
- 有限状态机的建模与优化设计 1次下载
- 基于VHDL的MTM总线主模块有限状态机设计 20次下载
- 基于有限状态机的虚拟训练过程模型研究
- fsm有限状态机pdf
- 什么是有限状态机?如何解决传统有限状态机「状态爆炸」问题? 5252次阅读
- SaberRD状态机建模工具介绍(一)什么是状态机建模 1249次阅读
- 什么是状态机?状态机的种类与实现 7941次阅读
- 一个基于事件驱动的有限状态机 673次阅读
- 嵌入式软件架构设计之状态机 1897次阅读
- 基于事件驱动的有限状态机介绍 941次阅读
- 嵌入式中状态机的设置 990次阅读
- 如何构建基于状态机的软件系统 1417次阅读
- 如何在Verilog中创建有限状态机 3284次阅读
- 基于有限状态机的FlexRay时钟同步机制 3293次阅读
- 使用层次型有限状态机对售货机控制器实现改造设计 2599次阅读
- 基于有限状态机的嵌入式系统串口通信帧同步方法设计 2461次阅读
- 状态机和组合逻辑的冒险竞争浅析 3876次阅读
- 利用74LS161实现复杂状态机 9057次阅读
- 初学者对有限状态机(FSM)的设计的认识 4142次阅读
下载排行
本周
- 1XL4015+LM358恒压恒流电路图
- 0.38 MB | 137次下载 | 1 积分
- 2PCB布线和布局电路设计规则
- 0.40 MB | 4次下载 | 免费
- 3TPS6287B25降压转换器评估模块
- 3.46MB | 1次下载 | 免费
- 4INA226EVM用户指南
- 4.7MB | 1次下载 | 免费
- 5INA226EVM修订版A模型用户指南和软件教程
- 2.28MB | 1次下载 | 免费
- 6Altium Designer印刷电路板设计与制作PDF电子书免费下载
- 14.11 MB | 0次下载 | 3 积分
- 7DLPC3470和DLPC3478软件编程人员指南
- 1.68MB | 次下载 | 免费
- 8TPS1213-Q1智能高侧驱动器评估模块
- 1.63MB | 次下载 | 免费
本月
- 1XL4015+LM358恒压恒流电路图
- 0.38 MB | 137次下载 | 1 积分
- 2新概念模拟电路第四册信号处理电路电子书免费下载
- 10.69 MB | 60次下载 | 免费
- 3800VA纯正弦波逆变器的参考设计
- 2.96MB | 34次下载 | 免费
- 4纯电动汽⻋的主要部件及⼯作原理
- 5.76 MB | 15次下载 | 5 积分
- 5JESD79-5C_v1.30-2024 内存技术规范
- 2.71 MB | 10次下载 | 免费
- 6elmo直线电机驱动调试细则
- 4.76 MB | 9次下载 | 6 积分
- 7明伟电源模块RSP-3000图纸
- 0.30 MB | 8次下载 | 免费
- 8使用BQ76PL102系列电量计进行BQ78PL114的快速入门指南
- 4.04MB | 7次下载 | 免费
总榜
- 1matlab软件下载入口
- 未知 | 935115次下载 | 10 积分
- 2开源硬件-PMP21529.1-4 开关降压/升压双向直流/直流转换器 PCB layout 设计
- 1.48MB | 420061次下载 | 10 积分
- 3Altium DXP2002下载入口
- 未知 | 233084次下载 | 10 积分
- 4电路仿真软件multisim 10.0免费下载
- 340992 | 191366次下载 | 10 积分
- 5十天学会AVR单片机与C语言视频教程 下载
- 158M | 183329次下载 | 10 积分
- 6labview8.5下载
- 未知 | 81581次下载 | 10 积分
- 7Keil工具MDK-Arm免费下载
- 0.02 MB | 73805次下载 | 10 积分
- 8LabVIEW 8.6下载
- 未知 | 65985次下载 | 10 积分
评论
查看更多