SMV在开发数字电视硬盘机顶盒中的应用

摘要：

数字电视硬盘机顶盒是一个逻辑复杂软件系统,因此,在逻辑模型设计阶段引入SMV工具分析其有限状态,就会从理论上保证了软件逻辑结构的正确.本文介绍了如何使用SMV方法及其软件对数字电视硬盘机顶盒的系统进行建模和分析,如何验证软件中各个线程的逻辑状态配置的正确和合理性.这种方法对软件开发中的有限状态分析有较大帮助。

关键词： 数字电视 硬盘机顶盒 数据广播 模型检验 SMV 数据轮 状态机

作者: 杨莹 王永滨 闫坚 于宁

作者单位: 中国传媒大学,计算机与软件学院,北京,100024

会议类型: 国内会议

会议名称: 第十次全国Petri网学术年会暨形式化方法学术讨论会

会议地点: 江苏镇江

会议语种:中文

页码: 190-192,203

在线出版日期: 2005-10-01（万方平台首次上网日期，不代表论文的发表时间）