Search

The learning and teaching power of the students in different courses can be different according to their intelligence and talent. A student may be smart in one course while being lazy in other courses. In order to increase the efficiency of a class, regardless of the class teacher, it is better to teach each course by the smartest student in that course. Inspired by this fact, we present a new meta-heuristic optimization algorithm called Participation of Smart Students (PSS) in increasing the class efficiency. To analyze the effectiveness of the PSS algorithm, we run it on 10 general test functions and 29 test functions from the 2017 IEEE Congress on Evolutionary Computation (CEC 2017). The results of PSS algorithm are compared with the effectiveness of Teaching and Learning-based Optimization (TLBO) Algorithm, Black Widow Optimization (BWO), Political Optimization (PO), Barnacle Mating Optimizer (BMO), Chimpanzee Optimization Algorithm (CHOA), Aquila Optimizer (AO) and City Council Evolution (CCE). Multiple comparison of the results obtained by the Friedman rank test shows that the PSS algorithm has a higher efficiency than the TLBO, BWO, PO, BMO, CHOA, and AO algorithms and almost similar efficiency as the CCE algorithm in terms of finding the closest solution to the optimal one and the hit rate. Moreover, the PSS algorithm has a higher convergence speed than all other algorithms.

Safety is one of the most important features of modern software systems, especially safety-critical systems such as nuclear power plants, which can be checked exactly by model checking. Model checking is a formal verification technique that analyzes system properties through exploring all reachable states (state space) of a model of a system. The problem of the technique is that it confronts the state space explosion in large and complex systems due to exponential memory usage. Recent researches show that a partial and intelligent exploration of the state space can be a suitable solution to overcome this problem. In this paper, we propose a two-phase model checking for safety analysis of systems specified formally through graph transformations. In the first phase, the beam-search algorithm explores the state space to a specific number of states. In case of failure of the phase, the second phase starts: in systems specified through graph transformations, the rule applied on the previous state can determine the rule that can perform on the next state. In other words, the rule on current state depends on only the rule applied to previous state, not the one on earlier states. Hence, a Markov chain (MC) is estimated to capture dependencies between the sequence of applied rules in the state space explored by the beam-search algorithm. The MC is then employed to explore the remainder of the state space intelligently. To evaluate the effectiveness of the two-phase model checking, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results show that the two-phase model checking has the high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques.

Model checking is one of the successful techniques in automated verification of software and hardware systems. However, employing this technique for verification of properties such as the safety and liveness requires that all possible states of a system are generated and then the given property is checked. In large and complex systems, generating all states causes the state space explosion problem. Hence, it is possible to refute such properties by searching the state space to find a state in which the given property is violated. Of course, it is possible that detecting such states in complex systems leads to the exhaustive exploration of the state space. Recent researches confirm that using meta-heuristic and evolutionary approaches to intelligently explore a portion of the state space can be a promising idea. Hence, in this paper, we propose an approach based on ant colony optimization algorithm for refuting the safety and liveness properties and also analyzing reachability ones in systems specified formally through graph transformation system. Refutation of liveness and analyzing reachability properties in systems modeled by graph transformations are the prominent advantages of this approach in comparison with the previous approaches. The proposed approach is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. Experimental results show that our proposed approach is faster and it generates shorter counterexamples in comparison with others.

Software architectural style is one of the best concepts to define a family of related architectures and their common properties. Despite the essential role of software architectures in the software engineering practice, the lack of formal description and analysis may hamper the quality of designed models. Hence, using proper formal languages seems necessary for architectural style description. In this case, it is possible to use model checking to verify the designed models automatically. However, the model checking of complex software systems suffers from the state space explosion problem. To handle this problem, data mining techniques may contribute to obtain the required knowledge for intelligent model checking i.e. searching only a portion of the state space. In this paper, to check the model of complex software systems which are designed according to an architectural style, an efficient approach is proposed using data mining techniques. These software systems must be specified through architectural styles and modeled by Graph Transformation Systems (GTS) formally. In the proposed approach, to check a large model based on a specific style intelligently, a specific knowledge is required. Such knowledge is acquired from mining the data of checking a smaller model consistent with the same style. These smaller models can be designed either by the designers or can be automatically generated consistent with the style. The proposed solution can be used to verify the reachability property and to refute the safety and liveness properties. This solution is implemented in GROOVE, a toolset for designing and model checking of graph transformation systems. The experimental results show that our method is faster and more accurate in comparison with the existing techniques in model checking of complex software systems.

Assessing the reliability of safety-critical systems is an important and challenging task because even a minor failure in these systems may result in catastrophic consequences, like losing human life. A well-known and fully automatic technique in reliability assessing approaches is model checking. However, applying this technique to verify some properties such as safety may lead to the state space explosion problem in which all reachable states cannot be checked due to computational limitations. In such situations that the verification of a safety property is infeasible, it is possible to refute the safety property by searching a reachable state in which a special configuration (e.g., an error or an undesirable behaviour) occurs. Therefore, checking reachability can be done instead of refuting the corresponding safety property. Finding such reachable states, in the worst case, may cause the state space explosion problem again. Hence, using evolutionary algorithms to explore the state space efficiently can be a promising idea. In this paper, at first, we propose an evolutionary algorithm to check reachability properties and refute safety ones in software systems specified formally through graph transformations. Since the accuracy and convergence speed of the proposed approach can still be improved, we employ the Bayesian Optimization Algorithm (BOA) to propose another approach. In BOA, a Bayesian network is learnt from the population and then sampled to generate new solutions. The proposed approaches can be used to analyse the reachability and safety properties. The proposed approaches are implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. To evaluate the efficiency of the proposed approaches, different benchmark problems are employed. Experimental results show that the proposed approaches are faster and more accurate than the existing methods.

An optimal algorithm is presented about Conflict-Free Coloring for connected subgraphs of chain of rings. Suppose the length of the chain is |C| and the maximum length of rings is |R|. A presented algorithm in [1] for a Chain of rings used O(log|C|.log|R|) colors but this algorithm uses O(log|C|+log|R|) colors. The coloring earned by this algorithm has the unique-min property, that is, the unique color is also minimum.