ارائه راهکاری جهت مقابله با مشکل انفجار فضای حالت در سیستم‌های تبدیل گراف با استفاده از الگوریتم‌های پرندگان و جستجوی گرانشی

نویسندگان

1 دانشجو

2 فارغ التحصیل

3 عضو هیئت علمی دانشگاه اراک

چکیده

چکیده: وارسی مدل، یک روش خودکار و راهکاری مناسب به­منظور درستی‌یابی سیستم‌های نرم‌افزاری مطمئن است. در این سیستم‌ها، نمی‌توان ریسک بروز خطا را حتی در فرآیند تست پذیرفت و لذا لازم است فرآیند درستی‌یابی، قبل از پیاده‌سازی و در سطح مدل انجام شود. سیستم‌های تبدیل گراف، از پرکاربردترین سیستم‌های مدل­سازی رسمی  و راهکاری مناسب به­منظور مدل­سازی و وارسی سیستم‌های پیچیده هستند. اما این سیستم‌ها در فرآیند وارسی مدل از مشکل انفجار فضای حالت رنج می‌برند که در صورت گسترده بودن ابعاد مسئله و لذا بزرگ شدن فضای حالت مدل، سیستم با کمبود حافظه مواجه می‌شود. لذا هدف از این پژوهش، پیشنهاد راهکاری جهت مقابله با این مشکل در فرآیند وارسی سیستم‌های تبدیل گراف است. راهکارهای ارائه­شده، به‌جای تولید کل فضای حالت، آن را در جهت رسیدن به یک حالت خطا به­طور مثال بن­بست، هدایت می‌کنند. راهکار پیشنهادی بر مبنای الگوریتم پرندگان  طراحی‌ شده‌ و برای جلوگیری از مشکل به دام افتادن در بهینه‌های محلی که مشکل اصلی این الگوریتم است، با الگوریتم جستجوی گرانشی که دارای قدرت خوبی در جستجوی محلی است، ترکیب ‌شده است. در نهایت  به‌منظور ارزیابی نتایج راهکارهای ارائه­شده، این راهکارها در ابزار Groove- از ابزارهای مدل­سازی تبدیل گراف-پیاده‌سازی شده‌اند.

کلیدواژه‌ها


[1]C. Baier and J.Katoen, Principles of Model Checking, MIT Press, 2008.
[2]A. Rensink, The GROOVE Simulator: A Tool for State Space Generation, Applications of Graph Transformations with Industrial Relevance (AGTIVE), 3062 LNCS (2003), 2003, pp. 479–485.
[3]H. Peng and S.Tahar, A Survey on Compositional Verification, Journal of circuits, systems, and computers, 1998.
[4]W. D. Roever, The Need for Compositional Proof Systems: A Servey, International Symposium on Compositionality: The Significant Difference, 1998, pp. 1-22.
[5]P. Wolper and P. Godefroid, Using partal orders for the efficient verification of deadlock freedom and safety properties, Formal Methods in System Design - Special issue on computer-aided verification:special methods II, 1991, pp.149-164.
[6]P. Godefroid, Using Partial orders to improve Automatic Verification Methods, 2nd International Workshop on Computer Aided Verification, 1991, pp. 176-185.
[7]E. M. Clarke, R. Enders, T. Filkorn, and S. Jha, Exploiting symmetry in temporal logic model checking, Formal Methods in System Design, 1996, pp. 77-104.
[8]V. Gyuris and A. Sistla, On-the-fly model checking under fairness that exploits symmetry, Formal Methods in System Design, 1999, pp. 217-238.
[9]E.A.Emerson, A.PSistla, and Weyl, Symmetry and Model Checking, 1996, pp. 105-131.
[10]G. Francesca, A. Santone, G. Vaglini, and M. L. Villani, Ant Colony Optimization for Deadlock Detection in Concurrent Systems, IEEE Computer Society, 2011, pp. 108-117.
[11]E. Alba and F. Chicano, Ant ColonyOptimization in Model Checking, 11th international conference on Computer aided systems theory, Springer-Verlag, 2007, pp. 523-530.
[12]R. Behjati, M. Sirjani, and M. N. Ahmadabadi, Bounded Rational Search for On-the-Fly Model Checking of LTL Properties, Fundamentals of Software Engineering,  5961 (2010), pp. 292-307.
[13]P. Godefroid and S. Khurshid, Exploring Very Large State Spaces Using Genetic Algorithms, Software Tools for Technology Transfer (STTT) - Special section on tools and algorithms for the construction and analysis of systems, 2004, pp. 117-127.
[14]E. Alba, F. Chicano, M. Ferreira, and J. Gomez-Pulido, Finding deadlocks in large concurrent java programs using genetic algorithms, 10th annual conference on Genetic and evolutionary computation, 2008, pp. 1735-1742.
[15]L. M. Duarte, L. Foss, R. Wagner, and T. Heimfarth, Model Checking the Ant Colony Optimisation, Distributed, Parallel and Biologically Inspired SystemsIFIP Advances in Information and Communication Technology, 329 (2010) 221-232.
[16]J. Kennedy and R. Eberhart, Particle Swarm Optimization, Proceedings of IEEE International Conference on Neural Networks, 1995, pp. 1942-1948.
[17]E. Rashedi, H. Nezamabadi-pour, and S. Saryazdi, GSA: A Gravitational Search Algorithm, Information Siences, 2009,pp. 2232-2248.
[18]C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design - Special issue on computer-aided verification: general methods, 1992, pp. 275-288.
[19]B. L. Webster, Solving combinatorial optimization problems using a new algorithm based on gravitational attraction, Florida Institue of Technology, 2004.
[20]D. Dill, U. Stern , A New Scheme for Memory-Efficient Probabilistic Verification, IFIPTC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 1996, pp. 333-348.
[21]U. Stern and D. Dill , Improved probabilistic verification by hash compaction, Correct Hardware Design and Verification Methods, 987 (1995), pp. 206-224.
[22]H. Sivaraja and G. Gopalakrishnan, Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking, Electronic Notes in Theoretical Computer Science, 89 (2003), pp. 51-67.
[23]P. Wolper and D. Leroy , Reliable hashing without collision detection, COMPUTER AIDED VERIFICATION.5TH INTERNATIONAL CONFERENCE, 1993, pp. 59-70.
[24]C. H. Yang, Prioritized Model Checking in, Stanford University, 1998.
[25]S. Edelkamp, A. L. Lafuente, S. Leue, Directed explicit model checking with HSF-SPIN, SPIN Workshop, 2001, pp. 57-79.
[26]C. Han. Yang. D.L.Dill, Validation with guided search of the state space, The 35th Annual Design Automation Conference, 1998.
[27]S. Edelkamp,S. Jabbar,A. L. Lafuente, Heuristic search for the analysis of graph transition systems, Graph Transformation (ICGT),  2006.
[28]G. J. Holzmann, The Modelchecker SPIN, IEEE Transactions on Software Engineering, 1997, pp. 279-295.
[29]R. Yousefian, V.Rafe, M.Rahmani, A Heuristic Solution for Model Checking Graph Transformation Systems, Applied Soft Computing, Elsevier, 24(2014), pp. 169-180.              
[30]G. Engels, J. H. Hausmann, R. Heckel, S. Sauer, Dynamic Meta Modeling: A Graphical Approach to the Operational Semantics of Behavioral Diagrams in UML, Springer, 2000, pp. 323-337.
[31]L. Baresi, R. Heckel, S. Thöne, D. Varro , Modeling and validation of service-oriented architectures: application vs. style, he 9th European Software Engineering Conference Held Jointly With 11th ACM SIGSOFT International Symposium On Foundations Of Software Engineering (ESEC/FSE-11), 2003, pp.68-77.
[32]S. Thone, R. Heckel, Behavioral Refinement of Graph Transformation-Based Models, Electronic Notes In Theoretical Computer Science (ENTCS), (2005), pp. 101-111.
[33]T. Mens, On the Use of Graph Transformations for Model Refactoring, in: Generative andTransformational Techniques in Software Engineering (GTTSE'05), Springer, (2005), pp. 219-257.
[34]G. Taentzer, K. Ehrig, E. Guerra, J. de Lara, L. Lengyel, T. Levendovszky, et al. K.Ehrig, Model Transformation by Graph Transformation: A Comparative Study, Workshop Model Transformation in Practice, Softwareand System modelings (Sosym), 2005.
[35]M. R. Nadaf. V. Rafe, Performance Modeling and Analysis of Software Architectures Specified Through Graph Transformations, Computing and Informatics, (2013), pp. 797-826.
[36]T. Isenberg, Bounded Model Checking of Graph Transformation Systems via SMT Solving, 2014.
[37]N. M. Sabri, M. Puteh, and M. R. Mahmood,  "A Review of Gravitational Search Algorithm" ,International Journal of Advance in Soft Computing, 5(2013), pp.1-39.
[38]E. Rashedi, H. Nezamabadi-pour, and S. Saryazdi, “Filter modeling using gravitational search algorithm,” Engineering Applications of Artificial Intelligence, 24(2011) , pp. 117–122.
[39]Z. Li-ping, Y. Huan-jun, and H. Shang-xu, Optimalchoice of parameters for particle swarm optimization, Journal of Zhejiang University SCIENCE A, 6 (2005) 528-534.
[40]R. Heckel, Graph Transformation in a Nutshell, Electronic Notes in Theorical Computer Sience (ENTCS), 148 (2006) 187-198.
[41]Y. Shi and R. Eberhart, A modified particle swarm optimizer, in: The International Conference on Evolutionary Computation, IEEE World Congress on Computational Intelligence,1998, pp. 69-73.
[42]Z. H. Zhan , S. Yat-sen , J. Xiao , J. Zhang , and W. N. Chen, Adaptive control of acceleration coefficients for particle swarm optimization basedon clustering analysis, Evolutionary Computation(CEC), 2007, pp. 3276-3282.
[43]D. Bratton and J. Kennedy, Defining a Standard for Particle Swarm Optimization, Swarm Intelligence Symposium, 2007. SIS 2007. IEEE, (2007), pp. 120-127.
[44]M. Settles, "An Introduction to Particle Swarm Optimization", University of Idaho, 1999.