受制于系统状态组合爆炸,并发系统的组合状态验证一直是困扰模型检验的难题。基于图形转换的组合框架,研究了该框架的组合状态安全性验证技术。采用Petri网模型构造系统组合框架,分析出组合系统可达状态空间与部件可达状态空间的包含关联关系,提出了组合状态危害等级分类模型,设计出组合状态可达性分析方法和层次化多级安全性验证算法,并实例应用于轨道交通列车控制系统的功能安全性验证。
Subject to the system state combinatorial explosion,compositional state verification of concurrent systems is also a difficult problem in model checking until now.A safety verification method of compositional states was proposed based on the combination framework of graph transformation.Using Petri net model as the components and connection of system combination framework,the contain relationship between reachable system compositional states and compo-nents state was analyzed.A hazard rating classification model of compositional states was proposed,and the composi-tional state reachability analysis methods and multi-level hierarchical safety verification algorithms were designed.Final-ly,the functional safety of rail transit train control system was verified by an example.