CAJ | 학술논문

受制于系统状态组合爆炸，并发系统的组合状态验证一直是困扰模型检验的难题。基于图形转换的组合框架，研究了该框架的组合状态安全性验证技术。采用Petri网模型构造系统组合框架，分析出组合系统可达状态空间与部件可达状态空间的包含关联关系，提出了组合状态危害等级分类模型，设计出组合状态可达性分析方法和层次化多级安全性验证算法，并实例应用于轨道交通列车控制系统的功能安全性验证。
수제우계통상태조합폭작，병발계통적조합상태험증일직시곤우모형검험적난제。기우도형전환적조합광가，연구료해광가적조합상태안전성험증기술。채용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.