Software testing is one of the key activities in software development life cycle that plays an important role in software quality. More than half of the software development costs and time are often spent on the test. Obviously, the automation of software testing, especially in generating test cases that is a key activity of this process, will dramatically reduce the costs. Among the prosperous testing techniques is model-based testing that utilizes model checker tools to automatically extract test cases. However, as these tools basically designed for model verification, not for test generation, the researches in the testing context are encountered with some major challenges such as state space explosion problem and duplication of the vast majority of test cases. In this paper, we propose a novel method using Beam-search algorithm for generating tests from systems specified through graph transformation specification. The popopsed approach not only improvs the mentioned challenges, but also generates the test suites with high coverage and low size in a desired time budget. We implemented it in the model checker tool GROOVE. To assess the efficiency of our approach, we compared it with model checker-assisted testing, search-based testing strategies and random testing. The empirical results over some case studies in the domain of service-oriented systems confirm it's superiority in terms of coverage size, test suit size and speed.

The model checking technique is a formal and effective method for verifying software systems, which analyses it via generating and examining all possible states of a model of the software system. In safety-critical systems, one could not admit the risk of error even in the testing process, therefore it is necessary to carry out the verification process before implementation and at the model level. Using this technique to evaluate properties such as security entails all available states (all state space) being generated, then the state space of the system in question be carefully examined. The main challenge of the model checking technique in large and complex systems with wide or infinite state space is the problem of state space explosion (lack of memory in the generation of all possible states). Graph transformation systems are one of the most widely used formal modeling systems and a suitable solution for modeling and checking complex systems. In systems where security property verification is not possible, the security feature can be refuted by searching for an accessible mode in which a specific configuration (e.g. error or undesirable behavior) occurs. Recent studies advocate that partial and intelligent exploration of part of the state space could be a good solution to the problem of state space explosion. The goal of this study is to use the random forest algorithm in the model checking which can solve the problem of state space explosion by selecting a few promising paths. A path is hopeful whenever the probability of reaching an answer through this path is higher than other paths. In the proposed method, a small model of the system is first created using the official language of the Graph Description System (GTS). Afterwards, a training data set of paths to the goal is generated from the small model mode space. The generated training data set is then provided to the random forest algorithm to identify and discover the logical relationships within it. In the next stage, the acquired knowledge is used to intelligently explore the incomplete space of the large model state. The proposed approach is used in the verification of the reachability property and to refute the safety feature in large and complex systems where it is impossible to generate the entire system state space. In order to evaluate the proposed approach, it has been implemented in GROOVE which is an open source tool for designing and checking models in graph conversion systems. The results indicate that the proposed method performs better than the compared methods in terms of average running time and the length of the generated witness.

The safety analysis of software systems, especially safety-critical ones, should be performed exactly because even a minor failure in these systems may result in disaster consequences. Also, such analysis must be done before implementation, i.e. the design step and in the model level. Model checking is an exact and mathematical-based way that gets a model of a system and analyzes it through exploring all reachable states of the model. Due to the complexity of some systems and their models, this way may face the state space explosion problem, i.e. it cannot explore all available states. A solution to solve this problem in these systems is that model checking tries to refute them, instead of verifying them, by finding errors such as deadlock (if available).Although, a heuristic has been previously proposed to find a deadlock in the model's state space and it has been applied in several simple heuristic search and evolutionary algorithms, its detection speed has been low. In this paper, we propose a novel heuristic to detect a deadlock in the model's state space, and test and compare its detection speed by applying it in several simple heuristic search algorithms such as iterative deepening A*, beam search, and evolutionary algorithms such as genetic, particle swarm optimization, and Bayesian optimization. Comparison results confirm that the new heuristic can detect a deadlock in less time than the previous heuristic.

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.

We may investigate the correctness of dynamic fuzzy models by a combination of Modal Temporal Logics and Fuzzy Logic. So far Fuzzy-extended Kripke structure (FzKripke) and Fuzzy-extended Program Graph (FzPG) are introduced as two timed Fuzzy logic models. Meanwhile, a Fuzzy-extended Temporal Logic (FzCTL) is introduced. Although no verification technique is devised for verifying FzCTL properties of timed Fuzzy logic models, its applications in verification of Fuzzy Logic Circuits (i.e., Fuzzy Flip-Flops) are studied and elaborated. In this paper we introduce a symbolic approach to tackle the state space explosion problem in timed Fuzzy logic models with which models are simultaneously compressed and processed in the most compact representation possible yet. The applicability of this approach is also demonstrated through experiments on a case study concerning dynamic hazards in a Fuzzy D-Flip Flop. Performance measures like runtime and memory consumptions are also provided for different scenarios.

One of the best solutions to verify software systems (especially critical systems) is model checking in which all reachable states are generated from an initial state and the generated state space is searched to find errors or some desirable patterns. However, the problem for many real and complex systems is the state space explosion in which model checking cannot generate all the states. In this paper, a solution is presented to cope with this problem in systems modeled by graph transformation. Since meta-heuristic algorithms are proper solutions to search in very large problem spaces, they employed in this research to find errors (e.g. deadlocks) in systems which cannot be verified through existing model checking approaches because of state space explosion problem. To do so, a Particle Swarm optimization (PSO) algorithm is empployed to consider only a subset of states (called population) in each step of the algorithm. To avoid local optima problem, PSO is combined with Gravitational Search Algorithm (GSA). Our proposed approach is implemented in GROOVE –a toolset for designing and model checking graph transformation system-. The experiments show better results in terms of accuracy, speed and memory usage in comparison with the existing approaches.

Model checking is among the most effective techniques for automatic verification of hardware and software systems’ properties. Generally, in this method, a model of the desired system is generated and all possible states are explored in the space state graph to find errors and undesirable patterns. In models of large and complex systems, if the size of the generated state space is too extensive so that not all available states can be explored due to computational restrictions, the problem of state space explosion occurs. In fact, this problem confines the validation process in model verification systems. To use the model checking technique, the system must be described in a formal language. Graphs are very beneficial and intuitive tools for describing and modeling software systems. Correspondingly, graph transformation system provides a proper tool for formal description of software system features as well as their automatic verification. Various techniques have been investigated in the researches to reduce the effect of state space explosion problem in the model checking process. Some of these methods try to reduce the required memory by reducing the number of cases explored. Among others are symbolic model checking, partial-order reduction, symmetry reduction, and scenario-driven model checking. In a complex system, these algorithms, along with conventional methods such as DFS or BFS search algorithms may not afford any complete answer due to the explosion of state space. Hence, the use of intelligent methods such as knowledge-based techniques, datamining, machine learning, and meta-heuristic algorithms which do not entail full state space exploration could be advantageous. Recent researches attest that exploring the state space using intelligent methods could be a promising idea. Therefore, an intelligent method is used in this research to explore the state space of large and complex systems. Accordingly in this paper, first a model of the desired system is created using graph conversion system. Then a portion of the state space of the model is generated. Afterwards, using the conditional probability table, the dependencies between the rules in the paths toward the goal state are discovered. Finally, by means of the discovered dependencies, the rest of the model state space is intelligently explored. In other words, only promising paths, i.e. those who match the detected dependencies are explored to reach the goal state. It is worth noting that the first goal of the proposed approach is to find a goal state, i.e., one in which either the safety property is violated or the reachability property is satisfied in the shortest possible time. The second less important goal is to reduce the number of explored states in the graph of the state space until reaching the goal state. This paper provides a way to check the availability feature in complex and large software systems modeled in the official graph transformation language. The suggested method is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. The results of experimental tests indicate that the proposed approach is faster than the previous methods and produces a shorter counterexample/witness.

Introduction For continuous years, academic and emotional functions were separate. This problem and cognitive - social changes occur in Adolescents (Spear, 2000) have been often associated with negative outcomes such as decreased academic value and interest, decreased mastery goals, increased stress, and lower academic achievement (Anderman & Anderman, 1999; Isakson & Jarvis, 1999; Roeser, Eccles, & Freedman-Doan, 1999; Rudolph, Lambert, Clark, & Kurlakowsky, 2001; Wigfield, Eccles, Schiefele, Roeser, & Davis-Kean, 2006). Thus, researchers interested in education have paid attention to the association of academic and emotional functions. According to Eccles and Roeser (2009) well-being is defined in relation to the school context and academic well-being includes four dimensions of School Value (is defined as the perceived meaningfulness of schooling in general), School burnout (is defined as consistency to school demands, cynical and detached attitude toward one's school, and feelings of inadequacy as a student (Salmela-Aro, Kiuru, Leskinen, &Nurmi, 2009), Satisfaction with educational choice (is defined as the student's satisfaction with his choice of education for attaining personal goals ), Schoolwork engagement (is defined as a positive, fulfilling, study-related state of mind that is characterized by vigor, dedication, and absorption (Salmela-Aro & Upadyaya, 2012). For creating and increasing academic wellbeing, attention to students and their personal agency is necessary. According to Bandura (2001), the personal agency is self-efficacy beliefs that in academic dimension nominate academic self-efficacy beliefs. Different research evidence has reported a positive relation between academic self-efficacy beliefs and academic self-esteem with academic well-being and success. According to Bandura (2001), Lazarus (1991) and Adler (1930), students with academic self-efficacy beliefs and academic self-esteem are active in school and more engaged with academic affairs. Consequently, the aim of the present study was to determine the possible relationship between academic self-efficacy beliefs and academic self-esteem with academic well-being and to test the mediating role of academic engagement in this regard.
Research questions The present study aimed at investigating the academic engagement mediatory role in the relation with academic self-efficacy beliefs and academic self-esteem and academic wellbeing. Therefore, the present study attempted to answer the following questions:- Is it possible to predict student's academic well-being based on academic selfefficacy beliefs and academic self-esteem?
- Is it possible to predict student's academic engagement according to academic selfefficacy beliefs and academic self-esteem?
- Can academic engagement have the mediatory role for academic self-efficacy beliefs and academic self-esteem as endogenous variables and academic well-being as an exogenous variable?
Method The study's design was a correlational. Academic self-efficacy beliefs and academic selfesteem as endogenous variables, academic engagement as a mediatory variable, and academic well-being as the final exogenous variable were considered for the enquiry. In this research, 384 students (186 females and 198 males) of a high school located in Poldokhtar county were chosen by multi-stage random cluster sampling method. In gathering data, The Persian versions of academic self-efficacy beliefs (ASEB, Zajacova, Lynch & Espenshade, 2005), academic self-esteem scale (ASES, Rosenberg, 1965), academic engagement scale (Salmela-Aro & Upadyaya, 2012) and academic well-being scale (AWBS, Heta, Katariina & Markku, 2012) have been used. All the research instruments enjoyed appropriate validity and reliability indices.
Results Path analysis showed that the academic self-efficacy beliefs and academic self-esteem predict academic engagement and academic well-being. Variable of academic engagement can play a mediatory role among academic self-efficacy beliefs, academic self-esteem and academic well-being.
Discussion In general, the findings of the study revealed the direct and the indirect effects of academic self-efficacy beliefs and academic self-esteem on the academic well-being. Not only has the academic engagement a direct effect on the academic well-being, it also acts as a mediatory variable between academic self-efficacy beliefs and academic self-esteem and academic well-being. Effective academic self-efficacy beliefs and academic self-esteem leads to creation and increase of academic engagement and with this increase, academic wellbeing increases. About significance and influence of self-regulation beliefs, Bandura (2001) maintains that none of the individual’s cognitive beliefs are constructive as efficacy in managing individual's compatibility performance in dealing with difficulties and stressful conditions. Students with high self-esteem in their performance appear more energetic and confident. Such a belief in confronting environmental stressful stimuli is accompanied by compatible performances of well-being. Finally, these findings emphasize the role of student's abilities, beliefs and attitudes in successful deal with impediments and academic challenges.

Providing all remote services requires mutual authentication of participating parties. The framework by which this authentication is done is called authentication protocols. In other words, cryptographic or cryptographic protocol is a distributed cryptographic algorithm that establishes interactions between at least two or more hosts with a specific purpose. In fact, these protocols have provided secure and insecure channels for communication between the parties participating in the protocol. Usually, secure channels are used for registration and insecure channels for mutual authentication. After registering on the server and verifying its identity by the server, the user can benefit from the services provided by the server. Many authentication protocols have been proposed in fields such as e-medical care, Internet of Things, cloud computing, etc. The privacy and anonymity of users in these plans is the biggest challenge in implementing a platform to benefit from remote services. Due to the fact that authentication of users takes place on the insecure platform of the Internet, it can be vulnerable to all existing Internet attacks. In general, there are two methods to analyze and prove the security of authentication protocols. Formal method and In-formal method. The In-formal method, which is based on intuitive arguments, analyst's creativity and mathematical concepts, tries to find errors and prove security. While the formal method, which is done both manually and automatically, has used a variety of mathematical logics and automatic security analysis tools. Manual method using mathematical models such as Real Or Random and mathematical logics such as BAN logic, GNY logic, etc., and automatic method using AVISPA, Scyther, ProVerif, TAMARIN, etc. tools. In fact, the methods of proving and analyzing the security of security protocols are divided into two general categories based on proof of theorem and model verification, and in this article, the details of each of these methods of proving security are explained. It should be noted that most of the security protocol verification tools are based on model verification. The methods based on model checking and then the methods based on proving the theorem are described.