Checking Reachability Property in Complex Concurrent Software Systems with a Knowledge Discovery Approach

doi:10.21203/rs.3.rs-738517/v1

Download PDF

Research Article

Checking Reachability Property in Complex Concurrent Software Systems with a Knowledge Discovery Approach

https://doi.org/10.21203/rs.3.rs-738517/v1

This work is licensed under a CC BY 4.0 License

Version 1

posted

You are reading this latest preprint version

The model checking technique is a formal and effectual way in verification of software systems. By generation and verification 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

The need to produce error-free systems concomitant with the increasing use of software in everyday life is more and more felt. Generating secure systems is of great importance especially in critical applications where any contingent error may lead to loss of many lives. Verification process in the critical applications should be carried out in the analysis and design phase prior to the implementation stage. Among other common ways, the checking model technique is employed as a formal verification approach seeking to find out whether the model of a system meets the predetermined requirements.

Graph transformation system is widely used in modelling, and allows us to describe system behaviour and states formally in the form of graphs and charts. The model checking, though an efficient approach in discovering the system's error, would encounter the state space explosion while needing to generate the whole state space of the model. When the problem's dimensions enlarge, the state space grows exponentially and the memory of the checking system could not produce, maintain, and deal with all states, contributing no avail to the checking process due to shortage of memory. Approaches are initiated in recent years to moderate the state space explosion. They include: Symbolic model checking [1] where the model is compressed and reduced in size using decision diagrams; Symmetry reduction [2] which merges those model states having structural similitude to make a smaller model; partial order reduction [3] which simplifies the models created by parallel ones so that by changing the execution order of the independent procedures, one could remove certain states; scenario-driven model checking [4] removes the states and transitions with no effects in the models based on graph transformation system and then sees to verification of the scenario; Abstract methods [5] merge the similar structures in the state space of the model and try to reduce the size of the latter.

All the approaches above aim to diminish the model state space and do not use any heuristics in the model checking. Notwithstanding the reduction of state space explosion by these methods, the shortage of memory and low speed yet hinder the model checking procedures in complex systems.

The rest of the paper is organized as follows. Section 2 includes a background of the related works, the description of the graph transformation system, and model checking. Section 3 dwells on the suggested method. The implementation and practical results pertaining to the suggested method together with those of the other methods are dealt with in Section 4. Advantages and drawbacks of the proposed method are discussed in Section 5. The last section is dedicated to the conclusion.

2.1 Related work

Smart methods have been recently employed for model checking. A* and Iterative Deepening A*(IDA*) algorithms are used in [6] to check the safety property in the system. In the present research, the Hemming distance between the current state and the goal state is regarded as the heuristic function and then implemented in HAF-APAIN tool to assess. The results indicate that this method is capable of checking the safety property by exploring fewer scenarios than SPAIN. The BDDA* approach given in [7] combines the breadth-first search algorithms with A* algorithm to avoid the exploration of unnecessary states. The results show a higher efficiency of this method in comparison with the breadth-first and depth-first search algorithms. In [8], the authors introduced the DFHS approach for checking the safety property of the system by adding a round back option to the breadth-first search algorithm. This approach is implemented and assessed in the checker of JPF model. The functionality of this method is proved to be much better than that of the breadth-first and depth-first search methods. A heuristics is applied in A* as well as the depth-first search methods by the authors of [9, 10] for checking reachability in the systems modeled by graph transformation. The heuristic function is designed on the basis of the structural similarity between the graph corresponding to the actual state and the ultimate state graph. This shows more enhanced outcomes relative to the depth-first and breadth-first search approaches. In [11, 12], a heuristic function is attained by the authors aimed at reducing the size of state space which can by applied in A* search, the depth-first search, and hill climbing to check the reachability property. The obtained results of this implementation tell of better efficiency compared to the previous techniques cited in [9, 10]. An approach to discover the deadlock error in the reaction systems is presented in [13] where, by the help of genetic algorithm, the search is directed towards the error states rather than the full state space. This is implemented and tested in VERISOFT- a search tool for the state space of the system and proved to be able to discover the error states in a shorter time in comparison with the random methods. A genetic-based way of discovering the dead end error is given in [14] founded on the graph transformation system in which each chromosome has a path of definite length in the state space. Applying mutation and crossover operators in the production of next-generation chromosomes, it aims to discover a path corresponding to the dead end state. Such a path, if any, would be reported as a counterexample. This attempt is guaranteed by the test results as to be successful in certain large models. In some huge and complex models, however, it comes to naught. In the reference [15], a technique was proposed to determine the dead end error in the systems described in terms of graph transformation. The approach is utilized to avoid getting caught in the local optimum trap through a combination of the bird and gravitational algorithms in the direction of the state space search. The estimation results in the GROOVE tool show that the above-mentioned technique is faster and more accurate than the depth-first and breadth-first search as well as the genetic-based algorithms. Another so-called BAPSO way to recognize the dead end state in the software systems is the proposed in [16] which uses bat and bird algorithms. The assessment of this method in GROOVE proves that it has a more proper efficiency than each of the bat and bird algorithms though having been failed in complex systems. The references [17, 18, and 19] ant-colony based methods are designed towards discovering the error state in the model checking process. Since the ant algorithm is set up on the ant's quest for food in the shortest way, generation of short-length discovering paths may be conducive to less storage space for the states. Overall, these approaches could have found the optimum or near-to- optimum responses. By using the bonus-based reinforcement learning, a new approach was proffered in [20] which has been applied in checking of the liveness property of the on-the-fly model. The checking of the on-the-fly model, unlike the ordinary one, is carried out simultaneously with the state space traversal. The results are indicative of insufficient accuracy and the low speed of this method compared to the meta-heuristic ones. In [21], the authors give a heuristic based on data mining to engage in checking safety, liveness, and reachability properties in the complex software systems. By discovering repetitive patterns of a small model of the problem, they could achieve the counterexample negating the above-mentioned properties in the large model. Enjoying though more speed and accuracy relative to the heuristic approaches, it hinges upon the small model of the problem and requires setting the initial parameters in the discovering function of repetitive patterns. By dint of the machine learning technique, the authors of [22] initiated a method for refutation of safety, liveness and verify of the reachability property. Thereupon, alongside the state space traversal, the interdependencies between the rules governing the state space are extracted by the Bayesian network to the purpose of the network enhancement. Then, the discovered knowledge arisen from the Bayesian network is applied to the traversal of the rest of the state space. The GROOVE results represent a good efficiency of this method compared with the evolutionary and meta-heuristic ones. This manner depends on the selection of the part of the state space used in learning the dependencies by the help of Bayesian network. Using the machine learning technique and discovering promise paths in the small model and traversal the paths in the large model thereafter, the authors of [23] have overcome the problem of state space explosion. In comparison with the evolutionary and heuristic methods, this scheme could generate the witness with a shorter length. In [24], while managing the state space in large and complex systems, the researchers achieved a higher accuracy in discovering dead end error via the n-gram technique. Requiring a relatively outsized space to store the n-gram table, this method is not so optimal as regards memory consumption.

Though the above-cited techniques have been able to fairly manage the issue of the state space explosion, the accuracy and speed of the convergence of the proposed methods are yet low especially in large and complex systems. Also, most approaches have only recognized the dead end while more complicated features such as reachability and liveness are still remained to be discussed. By smartening the model checking technique via the supervised machine learning algorithm, it is tried in this paper to achieve a higher efficiency than the previous methods as well as to make it possible to check the reachability property. In our suggested method, first the necessary knowledge is acquired about the operations changing the state of the system using the machine learning algorithm. Then, by the knowledge gained, the state space of the model is explored smartly.

2.2 Graph Transformation System

While model checking, it is necessary that the concerned system be described through a formal and intelligible modeling language. Among others, the graph transformation system comprises a triple GTS (TG, HG, R). Here, TG stands for type graph which shows all the elements in the software system, the labels of each element, and the relationship between the elements. HG designates the host graph representing the initial configuration of the system. The third component R signifies the set of transition rules. (When a rule is applied on one state of the system, the latter is transited from that state to another.)

The GROOVE tool has the capability of automatic checking through generating the state space of the problem. This tool is open source and features could be added to it. This is used here in modeling and analysis of software systems described by the official language of graph transformation.

As an example of a system modelled via GROOVE, one can mention the Dining Philosophers problem with 2 philosophers (see Fig. 1).

Part a represents the type graph TG. In this problem, there are two elements: philosopher and fork. The philosopher has the states (labels) of thinking, to be hungry, grabbing the left fork, grabbing the right fork, and eating. Part b is the host graph showing the configuration of dining two philosophers with two forks. The philosophers are flanked by forks set for common use. In the initial configuration, the position of the elements relative to each other is shown without any rules applied on the problem. In Part c, the rule get-left is applied. Thereupon, the edge labeled 'think' (the blue dotted edge) is removed and the edge with the label 'get-right' (the green edge) is created.

2.3 Model Checking

In model checking, first all the likely cases of the model are explored and then the correctness or incorrectness of the properties is ensured. In case the checking is done well (the state space explosion does not occur), a counterexample/witness is developed.

The counterexamples/witnesses report certain optimal /adverse behaviors of the system and could be used by the experts in fixing design flaws. Among others, safety and reachability property are important features of the software systems checked by this technique. The safety feature indicates that a good/bad item in an assumed system is absolutely true/false. Since the confirmation of this feature entails considering all the system's cases, it is tried that this property is refuted in the sense that an error is emerged in the state space. If so, the path from the beginning stage of the state space towards an error is called a counterexample. Reachability claims that there is a case in the state space in which the supposed property holds (goal state). In this case, the path from the beginning situation of the state space and ending this condition is referred to as a witness.

The proposed approach is designed in three following phases.

First phase: Checking the Small Model State Space

At this phase, a small model of the system is created before the state space is explored totally for checking the reachability property. The following operations are implemented duly.

A small model of the system in the form of the type graph is automatically or manually created by the designer.

The whole state space of the small model is made into a graph where the nodes are the states and the edges are the rules. To distinguish the goal and non-goal states, the state space is searched completely through the BFS algorithm. The state in which the reachability property holds is considered as the goal state. The BFS search is given in Algorithm 1.

Second Phase: training and Learning

The learning set is taught the machine learning algorithm to discover the logical relationships and the knowledge behind it. The operations below are carried out at this phase.

All the paths existing in the state space graph are extracted. Any path is generated as s0 r0 s1 r1…rl-1 sl where the si are the states and the ri represent the rules. s0 is taken as the initial state and sl is the state explored in the last breadth. Removing states from each path gives a sequence of rules. Each sequence as a training tuple along with the situation of reachability property in the corresponding path is labeled in the learning set so that any path satisfying the property is labeled 1 and otherwise it is labeled 0. The generation of the learning set is demonstrated in Algorithm 2.

The learning set is provided to the machine learning algorithm to discover the rules governing the state space and to acquire the relevant knowledge (training and learning operations). Algorithm 3 represents the learning set generation.

Algorithm 1. The BFS algorithm in GROOVE

1. Input: M : a model described by GTS;

2. Output: S : the state space of M;

3. GraphState state = the initial state of M;

4. LinkedList<GraphState> stateQueue=new LinkedList<GraphState> ();

5. stateQueue.enqueue (state);

6. S.nodes.add (state);

7. while stateQueue.size () > 0 do

8. state = stateQueue.dequeue ();

9. foreach MatchResult match in state.getMatches () do

10. GraphState next = state.applyMatch(match);

11. if next != null then

12. if !S.nodes.contains (next) then

13. stateQueue.enqueue (next);

14. S.nodes.add (state);

15. end if

16. S.edges.add (new Transition (state,match,next));

17. end if

18. end for

19. end while

20. return S;

Algorithm 2. The training dataset generator algorithm.

Input SM: a small model graph;

Output Dtr: training dataset;

foreach path in SM do

if reachability property has approved in the path Then

set label 1;

else

set label 0;

end if;

remove all state from the path;

add path into the Dtr;

end foreach;

return Dtr;

Third Phase: Smart Traversal of the Large Model

With due regard to the fact that checking all the paths in the state space sparks state space explosion, we shall choose only a few paths in a smart way by the knowledge obtained from the second phase and call them as the promise paths to be taken into account in the sequel. The following operations are done in the third phase.

We create the state space of the large model up to a certain level (up to the small model's level) and then we shall extract all the paths in the graph and place in the learning set. (Any path is an unlabeled test tuple.)

The learning set is supplied to the random forest learning algorithm to label the paths with 1 and 0 via the knowledge acquired from the small model's state space. Those labeled 1 are explored as the promise paths in the large model's state space, and if there is any goal state, they are shown as a confirmation sign of the reachability property. Hence, the smart and incomplete traversal of the large model's state space makes keeping away from the state space explosion. The smart engaging of the large model is given in Algorithm.

3. 3.1 Random Forest Learning

To enhance the accuracy, one could, among other ways, use a combination of models rather than resorting to just one model. The combination algorithms are those which take a set of models and merge their outputs to the purpose of making the ultimate learner such that its efficiency outshines that of each of the basic learners used in the algorithm. At last, the labels of the new records are determined by combining the output of each basic model used.

In the current paper, we take on the random forest combination approach. The classifications used in the random forest are all of the decision tree type. The general trend for generation of T decision trees is as follows. In each iteration (t=1, 2, …, T), a learning set Di is created by means of replacement sampling. Since the replacement sampling is adopted, it may be well happened that some tuples belong in Di more than once while some others are not present in this learning set. We denote the number of the special features used in determination of branches in each tree node by m which is less than those features at hand. Among these m special features, the one with the highest information gain is chosen as the special feature of the branch. Algorithm 4 shows the pseudocode of the random forest learning approach.

Algorithm 3. Intelligent checking of the large model.

Input: Dtr: training dataset, Dte: testing dataset, LM: large model;

Output: a witness for reachability property;

Rf= Random forest (Dtr);

foreach tuple in Dts do

if Rf.predict (tuple) equal 1 then

explore the tuple in the LM as promising path;

if current state is a goal state then

return the path as a witness;

end for;

endif;

end foreach;

Algorithm 4. Random forest-to create composite mode of classification.

Input: D, a set of N class-labeled training tuples. T, the number of tree. B, the number of nodes;

Output: A composite model;

for t=1:T do

Randomly sample the train data D with replacement to produce Di

Grow on unpruned decision tree.

for b=1:B do

Select m variable at random from the variable.

Pick the best variable with the highest information gain among the m.

Split the node into two daughter nodes.

end for

to make a prediction at a new tuple X:

return majority vote the prediction of the T tree.

This section is dedicated to assessing the efficiency of the proposed method for the verify of the reachability property. We have written the proposed approach in Java and implemented it in the open source GROOVE to evaluate the efficiency of the method and compare it with the other techniques. The new so-called 'machine learning' strategy is added to GROOVE in which the input parameters inclusive of the model itself are determined for checking and the desired depth with the aim of restriction of traversal. At the end of the implementation, one could observe the witness. Our the proposed method is assessed and compared with the approaches based on heuristic search such as: BS [25], BFS, and DFS, as well as with the meta-heuristic and evolutionary methods like GA [21], PSO, PSO-GSA [26] and the machine learning-based method [23]. The experiments are conducted in the GROOVE tool with the help of processor Intel® Core™ i5, with memory 3GB under Windows 8 Ultimate.

4.1 Benchmark

The suggested method was checked and performed on four well-known problems whose checking in the graph transformation systems is impossible due to largeness of the state space. The four problems dealt with in the present

paper are Dining Philosophers [27], Readers- Writers [28], N-Queens, and Process life-cycle [29].

Dining Philosophers

In this problem, n philosophers are sitting round a table with n forks. Each philosopher thinks, then gets hu

hungry and first grabs the left fork and then the right fork to start eating. Since each fork is shared by two adjacent philosophers, they compete to remove the forks.

Readers- Writers problem

In this problem, several processes compete with each other to access simultaneously to the common sources. Some processes play the role of readers of the sources and some others need to write in them. The rule is that several readers could read a source only if no writer is writing the source. Also, at any given moment, only one writer can write in one source.

N- Queen problem

This problem comprises N queens in an N×N chessboard. The queens must be so arranged in the board that they can not guard each other. Due to the movement of a queen horizontally, vertically, and obliquely in the chessboard, the queens each should be placed at different lengths, widths, and diameters to avoid be guarded.

Process life-cycle problem

In the life-cycle, after creating the process, should there is enough memory, it is loaded into memory and waits for CPU or I/O devices. Following the completion of the implementation, the process releases the resources at its disposal and stops.

4.2 Result and Analysis

Dining Philosophers Problem

The "dining philosophers" problem uses a small model with two philosophers for learning and modeling the state space. Here, the q-state is considered as "all philosophers grab the left fork and wait for the right fork". Table 1 shows the implementation results of all methods to approve the reachability property in q-state. Empirical experiments show that all methods are capable of recognizing the goal state in this problem. The proposed approach applied for larger models presents a superior efficiency than the other methods. The BS algorithm traverses the state space by both depth and surface simultaneously whence enjoying a high chance to find the state space.

Readers-Writers Problem

As for the Readers-Writers problem, two readers and two writers are taken up to make the small model presuming the q-state as "all readers/writers have ended up their processes". Owing to the fact that the state space of this problem is broad and wide, the BS algorithm takes a lengthy running time. The proposed approach has a better functionality in the larger models with respect to the other approaches. Table 2 gives the outcomes of all methods for verify of the reachability property of the q-state.

N-Queen Problem

Now, we turn to the N-queen problem for which a small 4×4 model is designed. The q-state here is read "all queens are located in the right position". Table 3 includes the implementation results of all approaches for verify of the reachability property of the q-state. Although only two rules govern this problem, the state space is broad and wide so that not a goal state can be recognized by the BS algorithm. The proposed approach takes a shorter running time especially in the larger models.

Process Life-Cycle Problem

The problem of process life-cycle works with a small model possessing 3 processes and 3 memories. The q state is assumed to be "all processes have completed their implementation". Table 4 represents the implementation of all approaches for gaining verify of the reachability.

property as regards the q state. In this problem, the goal states are deeply situated in the state space. Excluding the proposed method, all the other approaches are not able to find the goal state in the models with more than 12 processes. Prior to reach the goal state, the BS algorithm too faces lack of memory whence unsuccessful in attaining the goal state.

In the present paper, we consider the number of explored states in order to reach the goal state in the state space as another criterion comparing the efficiencies of the various approaches. To this purpose, we have chosen an example for each problem and the corresponding results are given in Table 5. As observed in Table 5 in most models the suggested method requires traversing of less number of states.

The proposed method has advantages in comparison with the other approaches. For instance, thanks to usage of the machine learning algorithm, the method does the checking of the model in an incomplete and more smartly fashion to steer clear of the state space explosion. To begin the checking operations, it also requires less initial parameters The proposed approach has a higher performance speed, explores a less number of states in the state space of the model, and generates a shorter witness.

The proposed method suffers a number of limitations as well. To mention some, its accuracy depends drastically on the small model of the problem the generation of which is difficult in some problems. The efficiency of the approach is extremely reliant on the capability of the machine learning algorithm in discovering knowledge from the small model's state space. Another disadvantage could be that this technique is not able to use the small model's knowledge to manage the large model's state space in dynamic environments where the governing conditions are frequently changing.

Model checking is an automatic and appropriate way to validate the software systems. One of the most widely-used formal modeling ideas in this respect is graph transformation system. The state space explosion is the most frequent trouble which the real and complicated systems are mainly encountered. In this article, we have given an approach that could traverse the state space of the model in an incomplete and smart way and does not undergo the state space explosion. According to our the proposed approach, a small model is created in the system at the outset. All the paths existing in the graph of the small model's state space are completely explored. Those ending in the goal state are labeled 1 and the rest are marked 0 in the learning set. Then, the learning set is taught to the random forest learning algorithm in order for discovering the logical relationships between the paths and their labels. Finally, the knowledge acquired during recognizing the promise paths of the large model is used to reach the goal state. The proposed method is also made used of to check the reachability property in the large and complicated systems. It is implemented in the GROOVE tool in Java language and compared to the heuristic, meta-heuristic, and evolutionary approaches. Doing the model checking in a more smartly manner, the proposed method needs less regulated parameters and shorter average time to perform. It generates the witness with a shorter length and explores less number of states in the state space than the other approaches. Dependence on the capability of the machine learning algorithm is among the restrictions hampering the proposed approach. In systems with dynamic state space undertaking no set rules, the approach retains no suitable efficiency.

Compliance with ethical standards

Conflict of interest The authors declare that there is no conflict of interest for any of them in this article.

Ethical approval This article does not contain any studies with human participants or animals performed by any of the authors.

H. Zhang, J. Du, L. Cao and G. Zhu. "A full symbolic reachability analysis algorithm of timed automata based on BDD in autonomous decentralized systems ", IEEE Twelfth International Symposium, pp. 301-304 (2015).
A. L. Lafuente. "Symmetry reduction and heuristic search for error detection in model checking", Workshop on Model Checking and Artificial Intelligence (2003).
A. L. Lafuente, S. Edelkamp, and S.Leue. "Partial order reduction in directed model checking", International SPIN Workshop on Model Checking of Software, Springer Berlin Heidelberg, pp. 112-127 (2002).
V. Rafe. "Scenario-driven analysis of systems specified through graph transformations", Journal of Visual Languages & Computing, vol. 24, no. 2, pp. 136-145 (2013).
A. Rensink and E. Zambon. "Pattern-based graph abstraction in Graph transformations", Springer Berlin Heidelberg, pp 66-80 (2012).
S. Edelkamp, A. L. Lafuente, and S. Leue. "Protocol verification with heuristic search", In AAAI Symposium on Model based Validation of Intelligence (2001).
S. Edelkamp and F. Reffel. "OBDDs in heuristic search", In Annual Conference on Artificial Intelligence, Springer Berlin Heidelberg, pp. 81-92 (1998).
J. Maeoka, Y. Tanabe, and F. Ishikawa. "Depth-First Heuristic Search for Software Model Checking", In Computer and Information Science, Springer International Publishing, pp. 75-96 (2016).
H. C. Estler and H. Wehrheim. "Heuristic search-based planning for graph transformation systems", KEPS, p. 54, (2011).
E. Snippe. "Using heuristic search to solve planning problems in GROOVE", In 14th Twente Student Conference on IT, University of Twente (2011).
S. Ziegert. "Graph Transformation Planning via Abstraction", arXiv preprint arXiv: 1407.7933 (2014).
J. W. Elsinga. "On a framework for domain independent heuristics in graph transformation planning", Master's thesis, University of Twente (2016).
P. Godefroid and S. Khurshid. "Exploring very large state spaces using genetic algorithms", In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp. 266-280, (2002).
R. Yousefian, V. Rafe, M. Rahmani, "a heuristic approach for model checking graph transformation systems", Appl. Soft Compute. Vol.24, pp. 169–180 (2014).
X. He, Z. Ma, W. Shao, G. Li. "A meta model for the notation of graphical modeling languages", In Computer Software and Applications Conference, COMPSAC. 31st Annual International, IEEE, vol. 1, pp. 219-224 (2007).
R. Yousefian, S. Aboutorabi, and V. Rafe. "A greedy algorithm versus meta heuristic solutions to deadlock detection in Graph Transformation Systems", Journal of Intelligent & Fuzzy Systems, vol. 13, no. 1, pp. 1-13 (2016).
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, pp. 1735-1742 (2008)
L. M. Duarte, L. Foss, R. Wagner, and T. Heimfarth, "Model Checking the Ant Colony Optimization, Distributed, Parallel and Biologically Inspired Systems" IFIP Advances in Information and Communication Technology, 329, pp. 221-232 (2010).
B. L. Webster, "solving combinatorial optimization problems using a new algorithm based on gravitational attraction", Florida Institute of Technology (2004).
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, pp. 292-307 (2010).
E. Pira, V. Rafe, A. Nikanjam. "EMCDM: efficient model checking by data mining for verification of complex software systems specified through architectural styles". Appl. Soft Compute. 44, pp. 1185–1201 (2016).
E. Pira, V. Rafe, A. Nikanjam. "Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm". Journal of System and Software,131, pp. 181-200 (2017).
J. Partabian, V. Rafe, H. Parvin, S.Nejatian "An Approach Based on Knowledge Exploration for State Space Management in Checking Reachability of Complex Software Systems", soft computing, vol. 24, pp.1-16 (2019).
M.Yasrebi, V. Rafe, H. Parvin, S.Nejatian "An efficient approach to state space management in model checking of complex software system using machine learning technique", journal of intelligent & Fuzzy system, vol.38, no. 2, pp. 1761-1773 (2020).
A. Groce and W. Visser. "Heuristics for model checking Java programs", International Journal on Software Tools for Technology Transfer (STTT), vol. 6, no. 4, pp. 260-276 (2004).
V. Rafe, M. Moradi, R. Yousefian, and A. Nikanjam. "A Meta-Heuristic Approach for Automated Refutation of Complex Software Systems Specified through Graph Transformations", Applied Soft Computing, vol. 33, pp. 136-149 (2015).
A. Schmidt. "Model Checking of Visual Modeling Languages", Master's Thesis, Budapest University of Technology, Hungary (2004).
J. H. Hausmann. "Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Techniques", PhD Thesis, Universität Paderborn, Germany (2005).
S. Ziegert. "Graph Transformation Planning via Abstraction", arXiv preprint arXiv: 1407.7933 (2014).

Tables 1 to 5 are available in the Supplementary Files section

Table1to5.docx

Download PDF

Version 1

posted

You are reading this latest preprint version

Checking Reachability Property in Complex Concurrent Software Systems with a Knowledge Discovery Approach

Status:

Version 1

Abstract

Figures

1. Introduction

2. Background

3. The Proposed Approach (Model Checking+ Random Forest)

4. Experimental Result

5. Advantages And Limitations Of The Proposed Approach

6. Conclusion

Declarations

References

Tables

Supplementary Files

Status:

Version 1