论文部分内容阅读
信息物理融合系统常采用嵌入式实时多任务系统作为其控制软件，这类软件的并发和非确定性给验证带来了困难．提出了一种利用统计模型检验技术分析多任务系统的功能正确性的方法．该方法构造的时间自动机模型以模块化的方式描述了实时多任务系统中的主要成分，包括实时操作系统、周期性任务、偶发任务、共享资源以及物理环境，能够展现多任务系统的细粒度的运行过程及其对物理环境的实时响应．应用该方法分析了玉兔号月球车控制软件的一个早期版本，发现了系统运行中出现的一个特殊错误，识别了实际系统出现错误的条件，再现了出现错误的场景．