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

作者：杨莹; 王永滨; 闫坚; 于宁机顶盒数据广播模型检验smv数据轮状态机

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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社