计算机科学技术学报 ›› 2021,Vol. 36 ›› Issue (4): 839-855.doi: 10.1007/s11390-020-1003-3

所属专题: Software Systems Theory and Algorithms

• • 上一篇    下一篇

用于基于模型的图形转换安全分析的Markov Chain分布估算算法

Einollah Pira   

  1. Faculty of Information Technology and Computer Engineering, Azarbaijan Shahid Madani University Tabriz 5375171379, Iran
  • 收稿日期:2019-10-06 修回日期:2020-10-11 出版日期:2021-07-05 发布日期:2021-07-30
  • 作者简介:Einollah Pira received his B.Sc. degree in computer engineering (software) from the University of Kharazmi, Tehran, Iran, 2000, his M.Sc. degree in computer engineering (software) from the Sharif University of Technology, Tehran, Iran, 2002, and his Ph.D. degree in computer engineering (software) from Arak University, Arak, Iran, 2017. Currently, he is an assistant professor with Department of Information Technology and Computer Engineering, Azarbaijan Shahid Madani University, Tabriz, Iran. His research interests include model checking, formal methods, software testing, and search-based software engineering.

Using Markov Chain Based Estimation of Distribution Algorithm for Model-Based Safety Analysis of Graph Transformation

Einollah Pira        

  1. Faculty of Information Technology and Computer Engineering, Azarbaijan Shahid Madani University Tabriz 5375171379, Iran
  • Received:2019-10-06 Revised:2020-10-11 Online:2021-07-05 Published:2021-07-30
  • About author:Einollah Pira received his B.Sc. degree in computer engineering (software) from the University of Kharazmi, Tehran, Iran, 2000, his M.Sc. degree in computer engineering (software) from the Sharif University of Technology, Tehran, Iran, 2002, and his Ph.D. degree in computer engineering (software) from Arak University, Arak, Iran, 2017. Currently, he is an assistant professor with Department of Information Technology and Computer Engineering, Azarbaijan Shahid Madani University, Tabriz, Iran. His research interests include model checking, formal methods, software testing, and search-based software engineering.

关键安全系统的可靠性评估能力是设计现代关键安全系统最重要的需求之一,在安全系统中,甚至一个小故障可能会降低使用寿命或者对环境造成不可修复的损坏。模型校验是一种通过探测某一模型所有可获取状态(状态空间)自动验证或驳回系统性能的技术。在大型复杂的系统里,很可能会发生状态空间爆炸的问题。通过图形转换探测系统的状态空间时,当前状态运用的规则明确可以在下一状态使用的规则。换句话说,当前状态允许使用的规则仅仅取决于前一状态使用的规则,而不是那些在它之前的状态规则。
这个事实促使我们使用Markov chain(MC)获取这种类型的依赖项并且使用分布评估算法(EDA)提升MC的质量。EDA是一种以每一代种群中最优个体学习和抽样概率模型指导最优解搜索的进化算法。为了验证本文所提出方法的效能,我们在GROOVE中执行它,GROOVE为一设计和模型校验图形转换系统的开源工具集。实验结果表明与指定通过图形转换的系统安全分析中现存元启发和进化技术相比,本文所提出的方法具有较高的速度和准确度。

关键词: 安全分析, 模型校验, Markov chain, 分布评估算法, 图形转换系统

Abstract: The ability to assess the reliability of safety-critical systems is one of the most crucial requirements in the design of modern safety-critical systems where even a minor failure can result in loss of life or irreparable damage to the environment. Model checking is an automatic technique that verifies or refutes system properties by exploring all reachable states (state space) of a model. In large and complex systems, it is probable that the state space explosion problem occurs. In exploring the state space of systems modeled by graph transformations, the rule applied on the current state specifies the rule that can perform on the next state. In other words, the allowed rule on the current state depends only on the applied rule on the previous state, not the ones on earlier states. This fact motivates us to use a Markov chain (MC) to capture this type of dependencies and applies the Estimation of Distribution Algorithm (EDA) to improve the quality of the MC. EDA is an evolutionary algorithm directing the search for the optimal solution by learning and sampling probabilistic models through the best individuals of a population at each generation. To show the effectiveness of the proposed approach, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results confirm that the proposed approach has a high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques in safety analysis of systems specified formally through graph transformations.

Key words: safety analysis, model checking, Markov chain, estimation of distribution algorithm, graph transformation system

[1] Rausand M. Reliability of Safety-Critical Systems:Theory and Applications. John Wiley & Sons, 2014. DOI:10.1002/9781118776353.
[2] Lahtinen J, Valkonen J, Björkman K, Frits J, Niemelä I, Heljanko K. Model checking of safety-critical software in the nuclear engineering domain. Reliab. Eng. Syst. Saf., 2012, 105:104-113. DOI:10.1016/j.ress.2012.03.021.
[3] Yousefian R, Rafe V, Rahmani M. A heuristic solution for model checking graph transformation systems. Appl. Soft Comput., 2014, 24:169-180. DOI:10.1016/j.asoc.2014.06.055.
[4] Francesca G, Santone A, Vaglini G, Villani M L. Ant colony optimization for deadlock detection in concurrent systems. In Proc. the 35th Annual IEEE International Computer Software and Applications Conference, July 2011, pp.108-117. DOI:10.1109/COMPSAC.2011.22.
[5] Alba E, Chicano F. Finding safety errors with ACO. In Proc. the 9th Annual Conference on Genetic and Evolutionary Computation, July 2007, pp.1066-1073. DOI:10.1145/1276958.1277171.
[6] Rafe V, Moradi M, Yousefian R, Nikanjam A. A metaheuristic solution for automated refutation of complex software systems specified through graph transformations. Appl. Soft Comput., 2015, 33:136-149. DOI:10.1016/j.asoc.2015.04.032.
[7] Pira E, Rafe V, Nikanjam A. Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm. J. Syst. Softw., 2017, 131:181-200. DOI:10.1016/j.jss.2017.05.128.
[8] Pira E, Rafe V, Nikanjam A. EMCDM:Efficient model checking by data mining for verification of complex software systems specified through architectural styles. Appl. Soft Comput., 2016, 49:1185-1201. DOI:10.1016/j.asoc.2016.06.039.
[9] Pira E, Rafe V, Nikanjam A. Searching for violation of safety and liveness properties using knowledge discovery in complex systems specified through graph transformations. Inf. Softw. Technol., 2018, 97:110-134. DOI:10.1016/j.infsof.2018.01.004.
[10] Bicarregui J, Matthews B. Proof and refutation in formal software development. In Proc. the 3rd Irish Workshop on Formal Methods, July 1999.
[11] Koller D, Friedman N. Probabilistic Graphical Models:Principles and Techniques (1st edition). MIT Press, 2009.
[12] Pelikan M, Goldberg D E, Cantú-Paz E. Linkage problem, distribution estimation, and Bayesian networks. Evol. Comput., 2000, 8(3):311-340. DOI:10.1162/106365600750078808.
[13] Lahtinen J, Kuismin T, Heljanko K. Verifying large modular systems using iterative abstraction refinement. Reliab. Eng. Syst. Saf., 2015, 139:120-130. DOI:10.1016/j.ress.2015.03.012.
[14] Rozenberg G. Handbook of Graph Grammars and Computing by Graph Transformation, Volume 1:Foundations. World Scientific, 1997. DOI:10.1142/3303.
[15] Kastenberg H, Rensink A. Model checking dynamic states in GROOVE. In Proc. the 13th International SPIN Workshop on Model Checking of Software, March 30-April 1, 2006, pp.299-305. DOI:10.1007/1169161719.
[16] Staunton J, Clark J A. Searching for safety violations using estimation of distribution algorithms. In Proc. the 3rd International Conference on Software Testing, Verification, and Validation, April 2010, pp.212-221. DOI:10.1109/ICSTW.2010.24.
[17] Staunton J, Clark J A. Finding short counterexamples in promela models using estimation of distribution algorithms. In Proc. the 13th Annual Conference on Genetic and Evolutionary Computation, July 2011, pp.1923-1930. DOI:10.1145/2001576.2001834.
[18] Staunton J, Clark J A. Applications of model reuse when using estimation of distribution algorithms to test concurrent software. In Proc. the 3rd International Symposium on Search Based Software Engineering, September 2011, pp.97-111. DOI:10.1007/978-3-642-23716-412.
[19] Pira E, Rafe V, Nikanjam A. Using evolutionary algorithms for reachability analysis of complex software systems specified through graph transformation. Reliab. Eng. Syst. Saf., 2019, 191:Article No. 106577. DOI:10.1016/j.ress.2019.106577.
[20] Yousefian R, Aboutorabi S, Rafe V. A greedy algorithm versus metaheuristic solutions to deadlock detection in graph transformation systems. J. Intell. Fuzzy Syst., 2016, 31(1):137-149. DOI:10.3233/IFS-162127.
[21] Yang X S. A new metaheuristic bat-inspired algorithm. In Proc. the 2010 Nature Inspired Cooperative Strategies for Optimization, May 2010, pp.65-74. DOI:10.1007/978-3-642-12538-66.
[22] Baier C, Katoen J P. Principles of Model Checking. MIT Press, 2008.
[23] Sivanandam S N, Deepa S N. Introduction to Genetic Algorithms. Springer, 2008. DOI:10.1007/978-3-540-73190-0.
[24] Groce A, Visser W. Heuristics for model checking Java programs. Int. J. Softw. Tools Technol. Transf., 2004, 6(4):260-276. DOI:10.1007/s10009-003-0130-9.
[25] Edelkamp S, Lafuente A L, Leue S. Protocol verification with heuristic search. In Proc. the 2001 Spring Symposium Series, March 2001.
[26] Schmidt Á. Model checking of visual modeling languages. Bp Univ Technol Hung. 2004.
[27] Bellovin S M, Cheswick W R. Network firewalls. IEEE Commun. Mag., 1994, 32(9):50-57. DOI:10.1109/35.312843.
[28] Azim M R S, Mahmud K, Das C K. Automatic train track switching system with computerized control from the central monitoring unit. International Journal of u-and eService, Science and Technology, 2014, 7(1):201-212. DOI:10.14257/ijunesst.2014.7.1.18.
[1] . [J]. , 2005, 20(2): 0-0.
[2] 张钹; 张铃;. The Complexity of Recognition in the Single-Layered PLN Network with Feedback Connections[J]. , 1993, 8(4): 31-35.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 周笛;. A Recovery Technique for Distributed Communicating Process Systems[J]. , 1986, 1(2): 34 -43 .
[2] 陈世华;. On the Structure of Finite Automata of Which M Is an(Weak)Inverse with Delay τ[J]. , 1986, 1(2): 54 -59 .
[3] 李万学;. Almost Optimal Dynamic 2-3 Trees[J]. , 1986, 1(2): 60 -71 .
[4] C.Y.Chung; 华宣仁;. A Chinese Information Processing System[J]. , 1986, 1(2): 15 -24 .
[5] 章萃; 赵沁平; 徐家福;. Kernel Language KLND[J]. , 1986, 1(3): 65 -79 .
[6] 王建潮; 魏道政;. An Effective Test Generation Algorithm for Combinational Circuits[J]. , 1986, 1(4): 1 -16 .
[7] 陈肇雄; 高庆狮;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[8] 黄河燕;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[9] 郑国梁; 李辉;. The Design and Implementation of the Syntax-Directed Editor Generator(SEG)[J]. , 1986, 1(4): 39 -48 .
[10] 黄学东; 蔡莲红; 方棣棠; 迟边进; 周立; 蒋力;. A Computer System for Chinese Character Speech Input[J]. , 1986, 1(4): 75 -83 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持:support@magtech.com.cn
总访问量: