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

Research on Composition Abstraction Refinement Verification for Real Time System

作　　者：梅佳[1] 王生原[1] 伍华健[2] 

机构地区：[1]清华大学计算机科学与技术系,北京100084 [2]桂林电子科技大学计算机科学与工程学院,广西桂林541004

出　　处：《小型微型计算机系统》2014年第7期1550-1555,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61272086)资助;广西自然科学青年基金项目(2012jjBAG0074)资助;广西混杂计算与集成电路设计分析重点实验室2012年度开放课题项目(2012HCIC05)资助;广西教育厅科研项目(201106LX840)资助;国家社会科学基金青年项目(11CTQ008)资助

摘　　要：实时系统已经广泛应用于人们工作生活中的各个领域,通常要求具有很高的可靠性,采用形式化方法对实时系统建模并验证是构建可信实时系统的重要手段.现有的实时系统大多是由组件构成的,为缓解组合形式验证中常见的状态爆炸问题,可以对实时系统组合模型运用时钟区域等价方法进行状态划分及合并,用构件抽象的组合建立构件组合的抽象并确保一致性,在验证过程中基于改进的反例引导的抽象精化框架对抽象模型进行精化以消除模型抽象可能引入的附加行为(伪反例).最后,以铁轨交通灯控制系统为例,通过相关实验进行数据分析与比较来说明方法的有效性.Real-time systems have been widely used in all areas for peoples＇ work and life and are often required high trust. Using formal methods modeling and verifying real-time system is an important means to build trusted real-time system. Most of the existing real-time systems are consist of components. To alleviate the state explosion problem in the composition formal verification,use clock region equivalence to divide and merge states for getting the abstract model. The abstraction model for the component composition can be built by composing the existential abstraction of components. On the premise of ensuring consistency,abstract model is refined by counter-example guided abstraction refinement framework that the additional behavior（spurious counter-example） can be eliminated.Finally,the traffic light control system of tracks is used as an example to illustrate the effectiveness of proposed method by experiments and data analysis.

关 键 词：时钟约束 组合模型 抽象精化验证 伪反例 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]