فهرست مطالب

مهندسی برق و مهندسی کامپیوتر ایران - سال بیستم شماره 1 (پیاپی 69، بهار 1401)

نشریه مهندسی برق و مهندسی کامپیوتر ایران
سال بیستم شماره 1 (پیاپی 69، بهار 1401)

  • ب - مهندسی کامپیوتر
  • تاریخ انتشار: 1401/04/18
  • تعداد عناوین: 8
|
  • احمدرضا منتظرالقائم* صفحات 1-12

    امروزه شبکه‏های چندرسانه‏ای بر روی اینترنت به یک جایگزین کم‌هزینه و کارامد برای PSTN تبدیل شده است. برنامه‏های کاربردی جهت انتقال مالتی‌مدیا بر روی بستر اینترنت روزبه‌روز فراگیرتر شده و به محبوبیت بسیار چشم‌گیری دست پیدا کرده‌اند. این ارتباط از دو فاز تشکیل شده است: فاز سیگنالینگ و فاز تبادل مدیا. فاز سیگنالینگ توسط پروکسی‌های SIP و فاز تبادل مدیا توسط سوییچ‏های شبکه انجام می‌شود. از مهم‌ترین چالش‌ها در شبکه‏های چندرسانه‏ای، اضافه‌بار شدن پروکسی‌های SIP و سوییچ‌های شبکه به ترتیب در فازهای سیگنالینگ و مدیا است. وجود این چالش سبب می‌شود که طیف وسیع کاربران شبکه با افت شدید کیفیت سرویس مواجه شوند. ما در این مقاله به مدل‌سازی مسیله مسیریابی در شبکه‏های چندرسانه‏ای جهت مقابله با اضافه‏بار می‏پردازیم. در این راستا یک روش مبتنی بر فناوری شبکه‌های نرم‌افزارمحور و بر پایه یک مدل برنامه‏ریزی ریاضی محدب در شبکه‏های چندرسانه‏ای ارایه می‏کنیم. روش پیشنهادی تحت سناریوها و توپولوژی‌های متنوع شبیه‌سازی می‌گردد و نتایج نشان می‌دهند که گذردهی و مصرف منابع، بهبود یافته است.

    کلیدواژگان: شبکه های نرم افزارمحور، کنترل اضافه بار، مدل سازی ریاضی، شبکه SIP، مدیریت منابع شبکه
  • راحیل براتی*، محمد صدرالساداتی، حمید سربازی آزاد صفحات 13-24

    پوشه‌ ثبات‌ بزرگ در پردازنده‌های گرافیکی با بهبود موازات سطح نخ، باعث کاهش دسترسی به حافظه‌ می‌شود. قبلا برای افزایش ظرفیت پوشه‌ ثبات با سربار توان و مساحت قابل قبول، روش LTRF ارایه شده است. معماری پوشه‌ ثبات LTRF دوسطحی است که از یک حافظه نهان ثبات و یک پوشه‌ ثبات اصلی استفاده می‌کند. ثبات‌های کلاف‌ها قبل از اجرای یک کلاف به حافظه نهان ثبات پیش‌واکشی می‌شوند. برای پیش‌واکشی ثبات‌ها، گراف کنترل جریان برنامه در سطح مترجم به زیرگراف‌هایی به نام بازه‌ثبات تقسیم می‌شود. یکی از سربار‌های روش LTRF انجام عمل پیش‌واکشی ثبات و تحمیل بیکاری کلاف در طول مدت پیش‌واکشی است که کاهش تعداد بازه‌ثبات به میزان چشم‌گیری این سربار را کاهش می‌دهد. اما تعداد ثبات‌ قابل استفاده در هر بازه‌ثبات محدود است و افزایش این تعداد در بازه‌ثبات منجر به افزایش ترافیک پیش‌واکشی و ظرفیت حافظه نهان می‌گردد که راه حل مناسبی برای کاهش تعداد بازه‌ثبات‌ها نیست. در این پژوهش به کمک بازتولید مقادیر میانی در زمان ترجمه سعی در کاهش تعداد ثبات‌های مورد نیاز در هر بازه‌ثبات داریم. نتایج شبیه‌سازی نشان می‌دهند که روش پیشنهادی ما، میزان تحمل‌پذیری تاخیر دسترسی به پوشه ثبات در روش LTRF را به میزان 29 درصد بهبود می‌بخشد. همچنین با به کار‌گیری یک پوشه ثبات سلول‌های حافظه DWM، معماری پیشنهادی قادر است که کارایی پردازنده گرافیکی مجهز به LTRF را به طور میانگین 18 درصد (حدود 30 درصد نسبت به معماری پردازنده گرافیکی پایه) افزایش دهد و این در حالی است که مقادیر انرژی و توان مصرفی به میزان 38 و 15 درصد کاهش می‌یابد.

    کلیدواژگان: پردازنده های گرافیکی، پوشه ثبات، بازتولید مقادیر، واحدهای اجرایی
  • محمدصادق کیهان پناه، بهروز کوهستانی* صفحات 25-35

    مقابله با آتش‌سوزی جنگل‌ها برای جلوگیری از خطرات بالقوه آنها و همچنین حفاظت از منابع طبیعی به عنوان یک چالش در میان محققان مطرح است. هدف از این تحقیق، تشخیص ویژگی‌های آتش و دود از تصاویر بصری پهپاد برای دسته‌بندی، تشخیص شیء و قطعه‌بندی تصاویر است. از آنجا که جنگل‌ها محیط‌های بسیار پیچیده و غیر ساختاری هستند، استفاده از سیستم بینایی همچنان با مشکلاتی نظیر شباهت ویژگی‌های شعله با نور خورشید، گیاهان و حیوانات و یا پوشش شعله با دود مواجه است که باعث هشدارهای اشتباه می‌شوند. روش پیشنهادی در این تحقیق، استفاده از شبکه‌های عصبی کانولوشنی از روش‌های یادگیری عمیق است که به صورت خودکار، توانایی استخراج یا تولید ویژگی در لایه‌های مختلف خود را دارند. ابتدا به جمع‌آوری داده و افزایش آنها با توجه به روش‌های داده‌افزایی پرداخته شده و در ادامه، استفاده از یک شبکه 12 لایه برای دسته‌بندی و همچنین روش یادگیری انتقالی برای قطعه‌بندی تصاویر پیشنهاد می‌شود. نتایج به دست آمده نشان می‌دهند که روش داده‌افزایی به کار برده شده با توجه به تغییر اندازه و آماده‌سازی تصاویر ورودی به شبکه از کاهش شدید ویژگی‌های موجود در تصاویر اولیه جلوگیری کرده و همچنین شبکه‌های عصبی کانولوشنی مورد استفاده می‌توانند به خوبی ویژگی‌های آتش و دود موجود در تصاویر را استخراج کنند و نهایتا به تشخیص و محلی‌سازی آنها بپردازند.

    کلیدواژگان: آتش سوزی جنگل، پردازش تصویر، شبکه عصبی کانولوشنی، یادگیری عمیق
  • افسانه شرفی، سپیده آدابی*، علی موقر، صلاح المجید صفحات 36-46

    امروزه فناوری اطلاعات همراه با گسترش روزافزون اینترنت اشیا، جهان فیزیکی را به تعامل بیشتر با محرک‌ها، حسگرها و دستگاه‌ها سوق داده است. نتیجه این تعامل، برقراری ارتباط "هر زمان و هر مکان" در دنیای واقعی است. خلا تحقیقی که بتواند در کنار فراهم‌ساختن پروتکلی چندلایه و بسیار امن (پروتکلی که هم‌زمان، کار شناسایی و احراز هویت را انجام می‌دهد) و در عین حال بار محاسباتی کمی داشته باشد، احساس می‌شود. بنابراین در حوزه سلامت و درمان و به منظور پایش از راه دور بیمارانی با معلولیت جسمی ‌و ذهنی (مانند بیماران فلج مغزی و قطع نخاع) نیاز مبرم به یک پروتکل بسیار امن وجود دارد. پروتکل پیشنهادی ما در این مطالعه یک پروتکل دولایه به نام "شناسایی- احراز هویت" می‌باشد که بر اساس EEG و اثر انگشت ساخته ‌شده است. همچنین مرحله احراز هویت ما، الگوریتم اصلاح‌شده دیفی- هلمن است. این الگوریتم به دلیل مشکل امنیتی (وجود نفر سوم) نیاز به اصلاح دارد که روش پیشنهادی با دریافت اثر انگشت و سیگنال EEG بیمار، با دقت بسیار بالا و سرعت بالایی قادر به انجام احراز هویت بیمار است. پروتکل پیشنهادی با استفاده از داده‌های 40 بیمار مبتلا به آسیب نخاعی ارزیابی ‌شده و نتایج پیاده‌سازی، امنیت بیشتر این پروتکل را نشان می‌دهد. صحت عملکرد این پروتکل مورد بررسی قرار گرفته و زمان پردازش آن در مرحله احراز هویت نیز به 0215/0 ثانیه کاهش یافته است.

    کلیدواژگان: اینترنت اشیا، احراز هویت، امنیت، سیگنال EEG
  • مهدی رجب زاده، ابوالفضل طرقی حقیقت*، امیرمسعود رحمانی صفحات 47-56

    استفاده از راهکارهای آگاه از انرژی از موضوعات مهم تحقیقاتی در حوزه رایانش ابری است. با کاربرد موثر الگوریتم‌ها‌ی جایگذاری و تجمیع ماشین‌ها‌ی مجازی، تامین‌کنندگان ابر قادر خواهند بود مصرف انرژی را کاهش دهند. در این مقاله مدل جدیدی ارایه شده که با بهبود در الگوریتم‌ها و ارایه روش‌های مناسب، به دنبال رسیدن به نتایج مطلوب است. نظارت دوره‌ای بر وضعیت منابع، تحلیل مناسب داده‌های به دست آمده و پیش‌بینی وضعیت بحرانی سرورها به کمک مدل مارکوف پیشنهادی سبب شده است که تا حد امکان از تعداد مهاجرت‌های غیر ضروری کاسته شود. ترکیب الگوریتم‌های ژنتیک و شبیه‌سازی تبرید در بخش جایگزینی در کنار تعریف زنجیره مارکوف جاذب باعث عملکرد بهتر و سریع‌تر الگوریتم پیشنهادی گردیده است. شبیه‌سازی‌های انجام‌شده در سناریوهای مختلف در کلودسیم نشان می‌دهد که در مقایسه با بهترین الگوریتم مورد مقایسه قرار گرفته، در بار کم، متوسط و زیاد، مصرف انرژی کاهش قابل توجهی داشته و این در حالی است که نقض توافقات سطح سرویس‌دهی نیز به طور متوسط 17 درصد کاهش یافته است.

    کلیدواژگان: الگوریتم های فرااکتشافی، رایانش ابری، زنجیره مارکوف جاذب، کاهش مصرف انرژی
  • ریحانه تقی زاده خانکوک، عباس ابراهیمی مقدم*، مرتضی خادمی صفحات 57-65

    در سامانه‌های کنترل ترافیک و ثبت تخلفات وسایل نقلیه همواره دستیابی به سامانه‌ای که بتوان با استفاده از آن به طور خودکار رفتارهای ناهنجار رانندگان را شناسایی کرد، چالشی اساسی به شمار می‌آید. در این تحقیق سامانه‌ای با مشخصات مذکور برای تشخیص ناهنجاری مسیر خودروها پیشنهاد گردیده که در آن ابتدا به استخراج ویژگی‌های زمانی- مکانی و تشکیل یک طبقه‌بند با کمک لغت‎نامه حاصل از آن ویژگی‌ها پرداخته می‌شود. طبقه‌بند از پردازش‌هایی چون خوشه‌بندی بهینه‌شده با الگوریتم جفت‌گیری زنبور عسل و پردازش تنک روی ویژگی‌های زمانی- مکانی حاصل از داده‌های آموزشی تشکیل می‌گردد. طبقه‌بند طراحی‌شده روی داده‌های آزمون، به منظور تشخیص ناهنجاری اعمال می‌شود. وجه تمایز این پژوهش نسبت به پژوهش‌های پیشین علاوه بر شیوه نوین در پیش‌پردازش صورت‌گرفته به منظور ایجاد ماتریس لغت‎نامه، تشخیص ناهنجاری بر پایه ارزیابی ماتریس حاصل از تعلق داده‌ها به هر طبقه است که منجر به دقت بالاتر روش پیشنهادی نسبت به سایر روش‌های رقیب می‌شود. برای ارزیابی بهتر روش پیشنهادی، ابتدا آن را روی پایگاه داده UCSD و سپس روی دنباله‌های ویدیویی استخراج‌شده از عبور و مرور خودروها در ضلع شمالی دانشگاه فردوسی مشهد اعمال نموده و سپس نتایج حاصل، با نتایج سایر پژوهش‌های شناخته‌شده در این حوزه مقایسه می‌گردد.

    کلیدواژگان: آموزش لغت نامه، استخراج ویژگی، بازسازی تنک تشخیص ناهنجاری
  • جواد حمیدزاده *، منا مرادی صفحات 66-72

    داده‌های جریانی متشکل از داده‌هایی است که به ترتیب و با سرعت و حجم زیاد به سیستم وارد می‌شوند. توزیع این داده‌ها ناپایدار بوده و در طول زمان ممکن است تغییر کنند. با توجه به اهمیت این نوع داده‌ها در حوزه‌هایی مهم نظیر اینترنت اشیا، تسریع عملکرد و افزایش توان عملیاتی تحلیل داده‌های بزرگ جریانی به عنوان موضوعی مهم، مورد توجه محققین است. در روش پیشنهادی، از مفهوم یادگیری ترکیبی برخط در مدل بهبودیافته ماشین یادگیر مفرط به منظور طبقه‌بندی داده‌های جریانی استفاده شده است. به دلیل استفاده از رویکرد افزایشی، در هر لحظه تنها یک بلوک داده بدون نیاز به دسترسی به داده‌های پیشین یاد گرفته می‌شود. همچنین با بهره‌گیری از رویکرد آدابوست، وزن‌دهی به طبقه‌بندی‌کننده‌های پایه و تصمیم‌گیری در مورد حفظ و یا حذف آنها بر اساس کیفیت پیش‌بینی‌ها انجام می‌شود. مزیت دیگر روش پیشنهادی، بهره‌گیری از رویکرد مبتنی بر صحت طبقه‌بندی کننده‌ جهت شناسایی رانش مفهوم است که منجر به تسهیل انطباق مدل و افزایش کارایی آن می‌شود. آزمایش‌ها بر روی مجموعه‌ داده‌های استاندارد انجام گردید و روش پیشنهادی به طور میانگین با کسب 90/0% خاص‌بودن، 69/0% حساسیت و 87/0% صحت توانست اختلاف معناداری با دو روش رقیب داشته باشد.

    کلیدواژگان: داده های جریانی، رانش مفهوم، ماشین یادگیری مفرط، یادگیری افزایشی
  • عین الله پیرا* صفحات 73-79

    تحلیل ایمنی سیستم های نرم افزاری، خصوصا از نوع بحرانی-ایمنی، باید بطور دقیق انجام شود چون که وجود حتی یک خطای کوچک در چنین سیستم هایی ممکن است نتایج فاجعه باری داشته باشد ضمنا چنین تحلیلی باید قبل از پیاده سازی یعنی در مرحله طراحی و در سطح مدل انجام شود. وارسی مدل یک روش دقیق و مبتنی بر ریاضی است که ایمنی سیستم های نرم افزاری را با دریافت مدلی از آن و بررسی تمام حالت های قابل دسترس مدل انجام می دهد. با توجه به پیچیدگی بعضی سیستم ها و مدل های آن، وارسی مدل ممکن است با مشکل انفجار فضای حالت مواجه شود. بنابراین، وارسی مدل بجای تایید ایمنی چنین سیستم هایی، آنها را با یافتن خطاهایی از جمله بن بست رد می-کند. اگر چه قبلا هیوریستیکی برای یافتن بن بست در فضای حالت مدل ارایه شده و آن را در چندین الگوریتم جستجوی مکاشفه ای ساده و تکاملی بکار برده اند ولی سرعت تشخیص آن پایین بوده است. در این مقاله، یک هیوریستیک جدید برای یافتن بن بست در فضای حالت مدل ارایه کرده و سرعت تشخیص آن را، با بکار بردن در الگوریتم های جستجوی مکاشفه ای ساده از جمله عمقی تکرار شونده A* و جستجوی پرتو و الگوریتم های تکاملی مختلف از جمله ژنتیک، بهینه سازی ازدحام ذرات و بهینه سازی بیزی با روش قبلی مقایسه می کنیم. نتایج مقایسه تایید می کنند که هیوریستیک جدید می تواند حالت بن بست را در زمان کمتری نسبت به هیوریستیک قبلی پیدا کند.

    کلیدواژگان: تحلیل ایمنی، وارسی مدل، بن بست، هیوریستیک، الگوریتم های تکاملی
|
  • Ahmadreza Montazerolghaem * Pages 1-12

    Nowadays, multimedia networks on the Internet have become a low-cost and efficient alternative to PSTN. Multimedia transfer applications on the Internet are becoming more and more popular. This connection consists of two phases: signaling and media. The signaling phase is performed by SIP proxies and the media phase by network switches. One of the most important challenges in multimedia networks is the overload of SIP proxies and network switches in the signaling and media phases. The existence of this challenge causes a wide range of network users to face a sharp decline in the quality of service. In this article, we model the routing problem in multimedia networks to deal with the overload. In this regard, we present a technology-based method of software-based networks and a mathematical programming model in multimedia networks. The proposed method is simulated under various scenarios and topologies. The results investigate that the throughput and resource consumption has improved.

    Keywords: SIP overload, mathematical modeling, multimedia network, routing problem, software-defined network technology
  • Rahil Barati*, Mohammad Sadrosadati Pages 13-24

    Large register files reduce the performance and energy overhead of memory accesses by improving the thread-level parallelism and reducing the number of data movements from the off-chip memory. Recently, the latency-tolerant register file (LTRF) is proposed to enable high-capacity register files with low power and area cost. LTRF is a two-level register file in which the first level is a small fast register cache, and the second level is a large slow main register file. LTRF uses a near-perfect register prefetching mechanism that warp registers are prefetched from the main register file to the register file cache before scheduling the warp and hiding the register prefetching latency by the execution of other active warps. LTRF specifies the working set of the warps by partitioning the control flow graph into several prefetch subgraphs, called register-interval. LTRF imposes some performance overhead due to warp stall during the register prefetching. Reducing the number of register-intervals can greatly mitigate this overhead, and improve the effectiveness of LTRF. A register-interval is a subgraph of the control flow graph (CFG) where it has to be a single-entry subgraph with a limited number of registers. We observe that the second constrain contributes more in reducing the size of register-intervals. Increasing the number of registers inside the register-interval cannot address this problem as it imposes huge performance and power overhead during the register prefetching process. In this paper, we propose a register-interval-aware re-production mechanism at compile-time to increase register-interval size without increasing the number of registers inside it. Our experimental results show that our proposal improves the effectiveness of LTRF by 29%, and LTRF’s performance by about 18% (about 30% improvement over baseline GPU architecture). Moreover, our proposal reduces GPU energy and power consumption by respectively 38% and 15%, on average.

    Keywords: GPUs, register file, value re-production, execution units
  • Mohammad Sadegh Kayhanpanah, Behrooz Koohestani * Pages 25-35

    Fighting forest fires to avoid their potential dangers as well as protect natural resources is a challenge for researchers. The goal of this research is to identify the features of fire and smoke from the unmanned aerial vehicle (UAV) visual images for classification, object detection, and image segmentation. Because forests are highly complex and nonstructured environments, the use of the vision system is still having problems such as the analogues of flame characteristics to sunlight, plants, and animals, or the smoke blocking the images of the fire, which causes false alarms. The proposed method in this research is the use of convolutional neural networks (CNNs) as a deep learning method that can automatically extract or generate features in different layers. First, we collect data and increase them according to data augmentation methods, and then, the use of a 12-layer network for classification as well as transfer learning method for segmentation of images is proposed. The results show that the data augmentation method used due to resizing and processing the input images to the network to prevent the drastic reduction of the features in the original images and also the CNNs used can extract the fire and smoke features in the images well and finally detect and localize them.

    Keywords: forest fire, unmanned aerial vehicles, image processing, deep learning, convolutional neural networks
  • Afsaneh Sharafi, Sepideh Adabi*, Ali Movaghar, Salah Al-Majed Pages 36-46

    Today, with the ever-expanding IoT, information technology has led the physical world to interact more with stimuli, sensors, and devices. The result of this interaction is communication "anytime, anywhere" in the real world. A research gap that can be felt in addition to providing a multi-layered and highly secure protocol (a protocol that simultaneously performs authentication) and at the same time has a low computational burden. Therefore, in the field of health and treatment and for the purpose of remote monitoring of patients with physical and mental disabilities (such as patients with cerebral palsy and spinal cord amputation) there is an urgent need for a very safe protocol. The protocol we propose in this study is a two-layer protocol called "Identification-Authentication" which is based on EEG and fingerprint. Also, our authentication step is the modified Diffie-Hellman algorithm. This algorithm needs to be modified due to a security problem (the presence of a third person) that the proposed method is able to authenticate the patient with very high accuracy and high speed by receiving the patient's fingerprint and EEG signal. The proposed protocol was evaluated using data from 40 patients with spinal cord injury. The implementation results show more security of this protocol, Validity of the proposed protocol is checked and the processing time of authentication stage is decrease to 0.0215 seconds.

    Keywords: Internet of things (IoT), authentication, security, EEG signal
  • mehdi rajabzadeh, Abolfazl Toroghi Haghighat *, Amir Masoud Rahmani Pages 47-56

    The use of energy-conscious solutions is one of the important research topics in the field of cloud computing. By effectively using virtual machine placement and aggregation algorithms, cloud suppliers will be able to reduce energy consumption. In this paper, a new model is presented that seeks to achieve the desired results by improving the algorithms and providing appropriate methods. Periodic monitoring of resource status, proper analysis of the data obtained, and prediction of the critical state of the servers using the proposed Markov model have reduced the number of unnecessary migrations as much as possible. The combination of genetic algorithm and simulated annealing in the replacement section along with the definition of the adsorbent Markov chain has resulted in better and faster performance of the proposed algorithm. Simulations performed in different scenarios in CloudSim show that compared to the best algorithm compared, at low, medium and high load, energy consumption has decreased significantly. Violations of service level agreements also fell by an average of 17 percent.

    Keywords: Meta heuristic algorithms, cloud computing, absorbing Markov chain, energy consumption
  • Reyhane Taghizade, Abbas Ebrahimi moghadam*, M. Khademi Pages 57-65

    In traffic control and vehicle registration systems a big challenge is achieving a system that automatically detects abnormal driving behavior. In this paper a system for detection of vehicle anomalies proposed, which at first extracts spatio-temporal features form clusters then creates dictionary from these features. This classification stage consists of processes such as, optimized clustering with the bee mating algorithm and sparse processing on spatiotemporal features derived from the training data. Finally the trained classifier is applied to the test data for anomaly detection. The distinction of this study from previous research is using new method of pre-processing to create a dictionary matrix and anomaly detection based on evaluation of matrix that related to each class dependency, which leads to higher accuracy of the proposed method compared to other leading methods. To evaluate the proposed method, UCSD database and video sequences recorded from vehicle traffic on Vakilabad Boulevard at the north side of Ferdowsi University of Mashhad are used and the performance of the proposed method is compare to other competing methods in this field. By analyzing the evaluation standards, we find that the proposed method performance is better than other methods.

    Keywords: Sparse reconstruction, feature extraction, learning, clustering
  • Javad Hamidzadeh*, Mona Moradi Pages 66-72

    Streaming data refers to data that is continuously generated in the form of fast streams with high volumes. This kind of data often runs into evolving environments where a change may affect the data distribution. Because of a wide range of real-world applications of data streams, performance improvement of streaming analytics has become a hot topic for researchers. The proposed method integrates online ensemble learning into extreme machine learning to improve the data stream classification performance. The proposed incremental method does not need to access the samples of previous blocks. Also, regarding the AdaBoost approach, it can react to concept drift by the component weighting mechanism and component update mechanism. The proposed method can adapt to the changes, and its performance is leveraged to retain high-accurate classifiers. The experiments have been done on benchmark datasets. The proposed method can achieve 0.90% average specificity, 0.69% average sensitivity, and 0.87% average accuracy, indicating its superiority compared to two competing methods.

    Keywords: Concept drift, data stream, extreme machine learning, incremental learning
  • Pages 73-79

    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.

    Keywords: Safety analysis, model checking, deadlock, heuristic, evolutionary algorithms