资料下载
×
中断驱动控制系统的检验
消耗积分:1 |
格式:rar |
大小:0.68 MB |
2018-01-23
分享资料个
针对一类中断驱动的航天控制系统，给出了有界模型检验的算法，这类系统由中断处理程序和操作系统调度的任务组成．当中断发生时，对应的中断处理程序响应中断事件，并可以修改控制变量值，以便在系统任务中完成后续工作．操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作．使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模，并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程．控制变量将中断处理过程和系统任务相关联，中断处理程序可以设定某个控制变量，而系统任务则通过检查该控制变量来确定是否需要进行后续处理．对于这样的形式化模型，给出了检验关键时序性质的有界模型检验算法．该算法使用深度优先的方式遍历所有长度小于等于K的可行路径，并使用SMT 23实现了对时间约束和规约的处理．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
