We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 36 Issue 4
July  2021
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
Einollah Pira. Using Markov Chain Based Estimation of Distribution Algorithm for Model-Based Safety Analysis of Graph Transformation[J]. Journal of Computer Science and Technology, 2021, 36(4): 839-855. DOI: 10.1007/s11390-020-1003-3
Citation: Einollah Pira. Using Markov Chain Based Estimation of Distribution Algorithm for Model-Based Safety Analysis of Graph Transformation[J]. Journal of Computer Science and Technology, 2021, 36(4): 839-855. DOI: 10.1007/s11390-020-1003-3
shu

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

  • Faculty of Information Technology and Computer Engineering, Azarbaijan Shahid Madani University Tabriz 5375171379, Iran

More Information
  • Author Bio:

    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.

  • Received Date: October 05, 2019
  • Revised Date: October 10, 2020
  • Published Date: July 04, 2021
    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.
    • FullText(HTML)
    • References (28)
  • [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.
    • Relative Articles

  • Related Articles

    [1]Momodou L. Sanyang, Ata Kabán. Large-Scale Estimation of Distribution Algorithms with Adaptive Heavy Tailed Random Projection Ensembles[J]. Journal of Computer Science and Technology, 2019, 34(6): 1241-1257. DOI: 10.1007/s11390-019-1973-1
    [2]Zhimin Gao, Lei Xu, Lin Chen, Xi Zhao, Yang Lu, Weidong Shi. CoC: A Unified Distributed Ledger Based Supply Chain Management System[J]. Journal of Computer Science and Technology, 2018, 33(2): 237-248. DOI: 10.1007/s11390-018-1816-5
    [3]Nan Ding, Shu-De Zhou, Zeng-Qi Sun. Histogram-Based Estimation of Distribution Algorithm: A Competent Method for Continuous Optimization[J]. Journal of Computer Science and Technology, 2008, 23(1): 35-43.
    [4]wang Zhenyu. ρ Graph: Rendezvous Ordering Graph forAda Concurrent Programs[J]. Journal of Computer Science and Technology, 1998, 13(6): 615-622.
    [5]Fu Yuxi. Reaction Graph[J]. Journal of Computer Science and Technology, 1998, 13(6): 510-530.
    [6]Wang Haohong, Wu Ruixun, Cai Shijie. A New Algorithm for Two-Dimensional Line Clipping via Geometric Transformation[J]. Journal of Computer Science and Technology, 1998, 13(5): 410-416.
    [7]Wang Kewen, Chen Huowang, Wu Quanyuan. The Least Fixpoint Transformation for Disjunctive Logic Programs[J]. Journal of Computer Science and Technology, 1998, 13(3): 193-201.
    [8]Gao Hong. Transformation List for SGML Application[J]. Journal of Computer Science and Technology, 1995, 10(5): 455-462.
    [9]Zhu Hong. Program Transformation by Solving Equations[J]. Journal of Computer Science and Technology, 1991, 6(2): 167-177.
    [10]Li Hao, Liu Qun. A Problem of Tree Graph[J]. Journal of Computer Science and Technology, 1989, 4(1): 61-66.
    • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(5)

    1. Einollah Pira, Vahid Rafe, Sajad Esfandyari. A three-phase approach to improve the functionality of t-way strategy. Soft Computing, 2024, 28(1): 415. DOI:10.1007/s00500-023-08199-5
    2. Minghui Sun, Smitha Gautham, Quanbo Ge, et al. Defining and characterizing model-based safety assessment: A review. Safety Science, 2024, 172: 106425. DOI:10.1016/j.ssci.2024.106425
    3. Pedro Larrañaga, Concha Bielza. Estimation of Distribution Algorithms in Machine Learning: A Survey. IEEE Transactions on Evolutionary Computation, 2024, 28(5): 1301. DOI:10.1109/TEVC.2023.3314105
    4. Yuyang Guo, Chu-ge Wu, Zhuo Li, et al. Permutation Optimization Using Multivariate Dependent Estimation of Distribution Algorithm. 2025 IEEE Symposia on Computational Intelligence for Energy, Transport and Environmental Sustainability (CIETES Companion), DOI:10.1109/CIETESCompanion65203.2025.11003333
    5. Máté Földiák. Probabilistic Graph Queries for Design Space Exploration Under Uncertainty. Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems, DOI:10.1145/3652620.3688199

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (61) PDF downloads (0) Cited by(5)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return