|
|
|
|
checking reachability property in complex concurrent software systems with a knowledge discovery approach
|
|
|
|
|
|
|
|
نویسنده
|
partabian jaafar ,bagherifard karamollah ,rafe vahid ,parvin hamid ,nejatian samad
|
|
منبع
|
رايانش نرم و فناوري اطلاعات - 2023 - دوره : 12 - شماره : 1 - صفحه:41 -51
|
|
چکیده
|
The model checking technique is a formal and effectual way in verification of software systems. by generation and investigation of all model states, it analyses the software systems. the main issue in the model checking of the complicated systems having wide or infinite state space is the lack of memory in generation of all states which is referred to as &state space explosion&. the random forest algorithm which is capable of knowledge discovery faces the above-cited problem by selecting a few promising paths. in our suggested method, first a small model of the system is developed by the formal language of graph transformation system (gts). a training data set is created from the small state space. the generated training data set is made available to the random forest algorithm to detect and discover the logical relationships existent in it. then, the knowledge acquired in this way is used in the smart and incomplete exploration of the large state space. the proposed approach is run in groove which is an open source tool for designing and studying the model of graph transformation systems. the results indicate that the suggested method in accordance with the two criteria (average running time and the number of explored states) performs better compared with the other approaches.
|
|
کلیدواژه
|
software systems verification ,knowledge discovery ,state space explosion ,model checking
|
|
آدرس
|
islamic azad university, lamerd branch, department of computer engineering, iran, islamic azad university, yasooj branch, department of computer engineering, iran, arak university, d faculty of engineering, department of computer engineering, iran, islamic azad university, nourabad mamasani branch, department of computer engineering, iran, islamic azad university, yasooj branch, department of electrical engineering, iran
|
|
پست الکترونیکی
|
samad.nej.2007@gmail.com
|
|
|
|
|
|
|
|
|
|
|
|
|
|
checking reachability property in complex concurrent software systems with a knowledge discovery approach
|
|
|
|
|
Authors
|
partabian jaafar ,bagherifard karamollah ,rafe vahid ,parvin hamid ,nejatian samad
|
|
Abstract
|
the model checking technique is a formal and effectual way in verification of software systems. by generation and investigation of all model states, it analyses the software systems. the main issue in the model checking of the complicated systems having wide or infinite state space is the lack of memory in generation of all states which is referred to as &state space explosion&. the random forest algorithm which is capable of knowledge discovery faces the above-cited problem by selecting a few promising paths. in our suggested method, first a small model of the system is developed by the formal language of graph transformation system (gts). a training data set is created from the small state space. the generated training data set is made available to the random forest algorithm to detect and discover the logical relationships existent in it. then, the knowledge acquired in this way is used in the smart and incomplete exploration of the large state space. the proposed approach is run in groove which is an open source tool for designing and studying the model of graph transformation systems. the results indicate that the suggested method in accordance with the two criteria (average running time and the number of explored states) performs better compared with the other approaches.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|