این سایت در حال حاضر پشتیبانی نمی شود و امکان دارد داده های نشریات بروز نباشند
پردازش علائم و داده ها، جلد ۲۰، شماره ۲، صفحات ۱۷۵-۱۹۴
عنوان فارسی وارسی ویژگی دسترس‌پذیری در سیستم‌های تبدیل گراف با رویکرد کشف وابستگی‌ شرطی بین قوانین
چکیده فارسی مقاله وارسی مدل[1] یکی از مؤثرترین تکنیک­های صحت سنجی خودکار ویژگی‌های سیستم‌های سخت‌افزاری و نرم‌افزاری است. در حالت کلی، در این روش، مدلی از سیستم موردنظر تولید می­شود و تمام حالات ممکن در گراف فضای حالت مورد کاوش قرار می‌گیرد تا بتواند خطاها و الگوهای نامطلوب را پیدا کند. در سیستم‌های بزرگ و پیچیده تولید تمام فضای حالت منجر به مشکل انفجار فضای حالت[2] می­شود. تحقیقات اخیر نشان می‌دهند که کاوش در فضای حالت با استفاده از روش‌های هوشمندانه، می‌تواند ایده امیدوارکننده‌ای باشد. ازاین‌رو در این تحقیق ابتدا مدلی از سیستم موردنظر ایجاد می‌شود، سپس بخشی از فضای حالت مدل، تولیدشده و با استفاده از احتمالات شرطی، وابستگی بین قوانین موجود در فضای حالت کشف می‌شوند. پس از آن، با کمک وابستگی‌های کشف‌شده، بقیه فضای حالت مدل را به‌طور هوشمندانه مورد کاوش قرار می‌گیرد. در این مقاله روشی برای وارسی ویژگی دسترس‌پذیری[3] در سیستم‌های نرم‌افزاری پیچیده و بزرگ که به زبان رسمی تبدیل گراف[4] (GTS) مدل شده‌اند، ارائه می‌شود. روش پیشنهادی در GROOVE که یک مجموعه ابزار منبع باز برای طراحی و بررسی وارسی مدل سیستم‌های تبدیل گراف می‌باشد، پیاده‌سازی شده است. نتایج آزمایش‌های تجربی نشان می‌دهند که رویکرد پیشنهادی نسبت به روش‌های قبلی سریع‌تر بوده و مثال‌های نقض[5]/شاهد[6]کوتاه‌تری تولید می‌کند. [1] Model checking [2] State space explosion [3] Reachability property [4] Graph transformation system [5] Counterexample [6] Witness  
کلیدواژه‌های فارسی مقاله وارسی مدل، انفجار فضای حالت، سیستم تبدیل گراف، جدول وابستگی شرطی، ویژگی دسترس‌پذیری
عنوان انگلیسی 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.
کلیدواژه‌های انگلیسی مقاله Model checking, State space explosion, Graph transformation system, Conditional probability table, Reachability property
نویسندگان مقاله جعفر پرتابیان | jaafar partabian


نشانی اینترنتی http://jsdp.rcisp.ac.ir/browse.php?a_code=A-10-1924-2&slc_lang=fa&sid=1
فایل مقاله فایلی برای مقاله ذخیره نشده است
کد مقاله (doi)
زبان مقاله منتشر شده fa
موضوعات مقاله منتشر شده مقالات پردازش داده‌های رقمی
نوع مقاله منتشر شده پژوهشی
برگشت به: صفحه اول پایگاه   |   نسخه مرتبط   |   نشریه مرتبط   |   فهرست نشریات