您的位置：山东大学 -> 科技期刊社 -> 《山东大学学报（理学版）》

山东大学学报（理学版） ›› 2014, Vol. 49 ›› Issue (09): 41-49.doi: 10.6040/j.issn.1671-9352.2.2014.139

• 论文 • 上一篇    下一篇

基于图形转换的组合状态安全性验证技术

杜军威, 江峰, 张会萍, 曹玲, 殷文文   

  1. 青岛科技大学信息科学技术学院, 山东 青岛 266061
  • 收稿日期:2014-06-24 修回日期:2014-08-27 出版日期:2014-09-20 发布日期:2014-09-30
  • 作者简介:杜军威（1974-），男，副教授，博士，研究方向为软件测试与验证技术.E-mail：djwqd@163.com
  • 基金资助:
    国家自然科学基金资助项目（61273180）；山东省自然基金资助项目（ZR2011FL17，ZR2011FQ005）；山东省高等学校科技计划项目（J11LG05）

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)

614

摘要： 受制于系统状态组合爆炸，并发系统的组合状态验证一直是困扰模型检验的难题。基于图形转换的组合框架，研究了该框架的组合状态安全性验证技术。采用Petri网模型构造系统组合框架，分析出组合系统可达状态空间与部件可达状态空间的包含关联关系，提出了组合状态危害等级分类模型，设计出组合状态可达性分析方法和层次化多级安全性验证算法，并实例应用于轨道交通列车控制系统的功能安全性验证。

关键词: Petri网, 安全性验证, 组合状态验证, 安全苛求系统, 图形转换

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

中图分类号: 

  • 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] 袁 杰,史海波,刘 昶,单玉刚,尚文利 . 基于模糊统计的模糊Petri网token确定方法[J]. J4, 2008, 43(3): 30-33 .
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
版权所有 © 2018 《山东大学学报(理学版)》编辑部　
地址: 山东省济南市山大南路27号山东大学中心校区（250100）　电话: +86-0531-88366917　E-mail: xblxb@sdu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发