وارسی ویژگی دسترس‌پذیری در سامانه های تبدیل گراف با رویکرد کشف وابستگی‌ شرطی بین قوانین

وارسی الگو یکی از موثرترین شیوههای صحت سنجی خودکار ویژگی های سامانه های سخت افزاری و نرم افزاری است. در حالت کلی در این روش الگویی از سامانه مورد نظر تولید می شود و تمام حالات ممکن در گراف فضای حالت کاوش میشود تا بتواند خطاها و الگوهای نامطلوب را پیدا کند در سامانه های بزرگ و پیچیده تولید تمام فضای حالت منجر به مشکل انفجار فضای حالت می شود. پژوهشهای اخیر نشان میدهند که کاوش در فضای حالت با استفاده از روشهای هوشمندانه می تواند پیشنهاد امیدوار کننده ای باشد؛ از این رو در این پژوهش نخست الگویی از سامانه مورد نظر ایجاد میشود ،سپس بخشی از فضای حالت الگو تولید شده و با استفاده از احتمالات شرطی وابستگی بین قوانین موجود در فضای حالت کشف می شوند پس از آن با کمک وابستگی های کشف شده، باقی فضای حالت الگو به طور هوشمندانه کاوش می شود در این مقاله روشی برای وارسی ویژگی دسترس پذیری در سامانه های نرم افزاری پیچیده و بزرگ که به زبان رسمی تبدیل گراف (gts) الگو شده اند ارائه می شود روش پیشنهادی در groove که یک مجموعه ابزار منبع باز برای طراحی و بررسی وارسی الگوی سامانه های تبدیل گراف است پیاده سازی شده است نتایج آزمایشهای تجربی نشان میدهند رویکرد پیشنهادی نسبت به روشهای قبلی سریع تر بوده و مثال های نقض شاهد کوتاه تری تولید می کند.

checking reachability property of systems specified through graph transformation with the approach of discovery conditional dependency between the rules

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.