Verification of Digital and Hybrid Systems

این کتاب از مدرسه تابستانی موسسه مطالعات پیشرفته ناتو که از 26 مه تا 6 ژوئن 1997 در آنتالیا، ترکیه برگزار شد. اجزای زمان منطقی و پیوسته این دوره در دو بخش تشکیل شد. بخش اول شامل اثبات قضیه، مدل‌های خودکار سیستم، منطق، ابزار و پیچیدگی تأیید می‌شود. بخش دوم مدل سازی و تایید سیستم های هیبریدی را پوشش می دهد. ه. سیستم‌هایی متشکل از یک بخش رویداد گسسته و یک بخش زمانی پیوسته که به روش‌های جدید با یکدیگر تعامل دارند. همراه با پیشرفت در میکروالکترونیک، روش های طراحی و ساخت سیستم های منطقی به تدریج پیچیده شده اند. یکی از راه‌های مقابله با مشکل حصول اطمینان از عملکرد بدون خطا سیستم‌های دیجیتال یا ترکیبی، استفاده از تکنیک‌های رسمی است. تمرین مقایسه مشخصات رسمی یک سیستم منطقی، یعنی آنچه که قرار است با توصیف عملیاتی رسمی آن انجام دهد - آنچه در واقع انجام می دهد! - به روشی خودکار یا نیمه خودکار، تأیید نامیده می شود. راستی‌آزمایی را می‌توان به شیوه‌ای پس از واقعیت انجام داد، به این معنی که پس از طراحی یک سیستم، مشخصات و شرح عملیاتی آن در صورت لزوم برای مطابقت با ابزار تأیید در دست بازسازی یا اصلاح می‌شوند و بررسی سازگاری انجام می‌شود.

This book grew out of a NATO Advanced Study Institute summer school that was held in Antalya, TUrkey from 26 May to 6 June 1997. The purpose of the summer school was to expose recent advances in the formal verification of systems composed of both logical and continuous time components. The course was structured in two parts. The first part covered theorem-proving, system automaton models, logics, tools, and complexity of verification. The second part covered modeling and verification of hybrid systems, i. e. , systems composed of a discrete event part and a continuous time part that interact with each other in novel ways. Along with advances in microelectronics, methods to design and build logical systems have grown progressively complex. One way to tackle the problem of ensuring the error-free operation of digital or hybrid systems is through the use of formal techniques. The exercise of comparing the formal specification of a logical system namely, what it is supposed to do to its formal operational description-what it actually does!-in an automated or semi-automated manner is called verification. Verification can be performed in an after-the-fact manner, meaning that after a system is already designed, its specification and operational description are regenerated or modified, if necessary, to match the verification tool at hand and the consistency check is carried out.