实时系统组合抽象精化验证研究

实时系统已经广泛应用于人们工作生活中的各个领域,通常要求具有很高的可靠性,采用形式化方法对实时系统建模并验证是构建可信实时系统的重要手段.现有的实时系统大多是由组件构成的,为缓解组合形式验证中常见的状态爆炸问题,可以对实时系统组合模型运用时钟区域等价方法进行状态划分及合并,用构件抽象的组合建立构件组合的抽象并确保一致性,在验证过程中基于改进的反例引导的抽象精化框架对抽象模型进行精化以消除模型抽象可能引入的附加行为(伪反例).最后,以铁轨交通灯控制系统为例,通过相关实验进行数据分析与比较来说明方法的有效性.