محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
اینستاگرام تی پی بین
همایش ، رویداد ، ژورنال
  • جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 762
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     in this paper we investigate to what extent a very simple and natural “reachability as deducibility” approach, originating in research on formal methods for security, is applicable to the automated verification of large classes of infinite state and parameterized systems. in this approach the verification of a safety property is reduced to the purely logical problem of finding a countermodel for a first-order formula. this task is delegated then to generic automated finite model building procedures. a finite countermodel, if found, provides with a concise representation for a system invariant sufficient to establish the safety. in this paper we first present a detailed case study on the verification of a parameterized mutual exclusion protocol. further we establish the relative completeness of the finite countermodel finding method (fcm) for a class of parameterized linear arrays of finite automata with respect to known methods based on monotonic abstraction and symbolic backward reachability. the practical efficiency of the method is illustrated on a set of verification problems taken from the literature using mace4 model finding procedure.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها