JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE) ›› 2014, Vol. 49 ›› Issue (09): 41-49.doi: 10.6040/j.issn.1671-9352.2.2014.139

Previous Articles     Next Articles

A safety verification method of compositional states based on graph transformation

DU Jun-wei, JIANG Feng, ZHANG Hui-ping, CAO Ling, YIN Wen-wen   

  1. School of Information Science and Technology, Qingdao University of Science and Technology, Qingdao 266061, Shandong, China
  • Received:2014-06-24 Revised:2014-08-27 Online:2014-09-20 Published:2014-09-30

PDF (PC)

571

Abstract: 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 components state was analyzed. A hazard rating classification model of compositional states was proposed, and the compositional state reachability analysis methods and multi-level hierarchical safety verification algorithms were designed. Finally, the functional safety of rail transit train control system was verified by an example.

Key words: safety verification, composite state verification, graph transformation, safety-critical system, Petri net

CLC Number: 

  • TP309
[1] CENELEC. EN50129: railway applications-safety related electronic systems for signaling[S]. The European Standard, 2003.
[2] 郦萌,吴芳美. 铁路信号可靠性安全性理论及证实[M]. 北京:中国铁道出版社,2008. LI Meng, WU Fangmei. Reliability of railway signal safety theory and confirmed[M].Beijing: Chinese Railway Publishing House, 2008.
[3] EHRIG K, PRANGE U, TAENTZER G. Fundamentals of algebraic graph transformation[M]. Heidelberg: Springer, 2006.
[4] GUERRA E, DE LARA J, KOLOVOS D S, et al. Engineering model transformations with transML[J]. Software and Systems Modeling, 2013, 12(3):555-577.
[5] MEHNER-HEINDL K, MONGA M, TAENTZER G. Analysis of aspect-oriented models using graph transformation systems[J]. Aspect-oriented Requirements Engineering, 2013:243-270.
[6] PADBERG J, EHRIG H. Petri net modules in the transformation-based component framework [J]. The Journal of Logic and Algebraic Programming, 2006, 67(1/2): 198-225.
[7] EHRIG H, PADBERG J, OREJAS F, et al. A generic framework for connector architectures based on components and transformation proc[EB/OL]. [2017-03-12].http://www.researchgate.net/publication/220370614.
[8] OREJAS F, EHRIG H, KLEIN M, et al. A generic approach to connector architectures part I: the general framework[J]. Fundamenta Informaticae, 2010, 99(1): 63-93.
[9] KUSKE S. A formal semantics of UML state machines based on structured graph transformation[M]. Lecture Notes in Computer Science, 2001, 2185:241-256.
[10] STRBER D, TAENTZER G, JURACK S, et al. Towards a distributed modeling process based on composite models [C]// Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering. Berlin, Heidelberg: Springer, 2013: 6-20.
[11] 杜军威,徐中伟,喻钢.基于图形转换的构件组装研究与应用[J].同济大学学报:自然科学版,2009, 37(5):680-684, 695. DU Junwei, XU Zhongwei, YU Gang. Research and application of component composition based on graph transformation [J]. Journal of Tongji University: Natural Science, 2009, 37(5): 680-684, 695.
[12] BRANDT C, HERMANN F. Conformance analysis of organizational models:a new enterprise modeling framework using algebraic graph transformation[J]. International Journal of Information System Modeling and Design, 2013, 4(1): 42-78.
[13] ANJORIN A, SALLER K, LOCHAU M, et al. Modularizing triple graph grammars using rule refinement[C]// Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering. Berlin, Heidelberg:Springer, 2014: 340-354.
[14] HERMANN F, EHRIG H, OREJAS F, et al. Formal analysis of functional behaviour for model transformations based on triple graph grammars[J]. Lecture Notes in Computer Science, 2010, 6372: 155-170.
[15] PETRIU D C, SHEN Hui, SABETTA A. Performance analysis of aspect-oriented UML models[J]. Software & Systems Modeling, 2007, 6(4): 453-471.
[16] JURACK S, TAENTZER G. Transformation of typed composite graphs with inheritance and containment structures [J]. Fundamenta Informaticae, 2012, 118(1/2): 97-134.
[17] LEVESON N G, STOLZY J L. Safety analysis using Petri nets[J]. IEEE Transactions on Software Engineering, 1987, SE-13(3): 386-397.
[18] 杜军威,徐中伟,王树梅.联锁逻辑模型的安全性分析[J].计算机工程与应用,2007, 43(2):1-4, 32. DU Junwei, XU Zhongwei, WANG Shumei. Safety analysis of interlocking logic model[J]. Computer Engineering and Applications, 2007, 43(2): 1-4, 32.
[19] WU Jianing, YAN Shaoze, XIE Liyang. Reliability analysis method of a solar array by using fault tree analysis and fuzzy reasoning Petri net[J]. Acta Astronautica, 2011, 69(11/12): 960-968.
[1] ZOU Jin-yu, REN Hai-zhen. The total number of matchings of L*n,p [J]. J4, 2013, 48(2): 49-52.
[2] YUAN Jie,SHI Hai-bo,LIU Chang,SHAN Yu-gang,SHANG Wen-li . Determination of fuzzy tokens in fuzzy Petri nets based on fuzzy statistics [J]. J4, 2008, 43(3): 30-33 .
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
Copyright 2018 © Editorial office of JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE)
Supported by Beijing Magtech Co.Ltd